huge commit in automation:

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

diff --git a/helm/software/matita/library/nat/times.ma b/helm/software/matita/library/nat/times.ma
index 8de22c1e3c1d4c4c7867cbe24c08b4c6575ef006..f59622218e84c38535f862a7f8917fd7a5b4d87d 100644 (file)
--- a/helm/software/matita/library/nat/times.ma
+++ b/helm/software/matita/library/nat/times.ma
@@ -1,3 +1,4 @@
+
 (**************************************************************************)
 (*       __                                                               *)
 (*      ||M||                                                             *)
@@ -37,7 +38,7 @@ theorem times_n_Sm :
 intros.elim n.
 simplify.reflexivity.
 simplify.
-demodulate all steps=3.
+demodulate all.
 (*
 apply eq_f.rewrite < H.
 transitivity ((n1+m)+n1*m).symmetry.apply assoc_plus.
@@ -112,7 +113,7 @@ unfold distributive.
 intros.elim x.
 simplify.reflexivity.
 simplify.
-demodulate all steps=16.
+demodulate all.
 (*
 rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus.
 apply eq_f.rewrite < assoc_plus. rewrite < (sym_plus ? z).
@@ -127,7 +128,7 @@ unfold associative.
 intros.
 elim x. simplify.apply refl_eq. 
 simplify.
-demodulate all steps=4.
+demodulate all.
 (*
 rewrite < sym_times.
 rewrite > distr_times_plus.