]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/library/nat/log.ma
Removed final question marks from {apply|elim|rewrite}s.
[helm.git] / helm / matita / library / nat / log.ma
index 301c0be8ef1dc689646af66e4321177c2cb5372f..3babb5c75151fe36f0cf098e055d39294164eb22 100644 (file)
@@ -178,7 +178,7 @@ rewrite > H4.
 (* META NOT FOUND !!!  
 rewrite > sym_eq. *)
 simplify.intro.
-apply not_eq_O_S m1 ?.
+apply not_eq_O_S m1.
 rewrite > H5.reflexivity.
 qed.