1. PrimitiveTactics.new_metasenv_for_apply changed a little bit, moved to

[helm.git] / helm / matita / library / nat.ma

diff --git a/helm/matita/library/nat.ma b/helm/matita/library/nat.ma
index 4ab1feb2b84873e1898cc9e1c3ed68de98b9fe1e..c125e6775b7a2f48604f5912dad0f7c2c5defde6 100644 (file)
--- a/helm/matita/library/nat.ma
+++ b/helm/matita/library/nat.ma
@@ -36,8 +36,8 @@ qed.
 theorem injective_S : \forall n,m:nat. 
 (eq nat (S n) (S m)) \to (eq nat n m).
 intros;
-rewrite > pred_Sn n;
-rewrite > pred_Sn m;
+rewrite > pred_Sn;
+rewrite > pred_Sn m.
 apply f_equal; assumption.
 qed.
 
@@ -112,7 +112,7 @@ qed.
 theorem sym_times : 
 \forall n,m:nat. eq nat (times n m) (times m n).
 intros.elim n.simplify.apply times_n_O.
-simplify.rewrite < sym_eq ? ? ? H.apply times_n_Sm.
+simplify.rewrite > H.apply times_n_Sm.
 qed.
 
 let rec minus n m \def