X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Ftimes.ma;h=f59622218e84c38535f862a7f8917fd7a5b4d87d;hb=68dbcd02022874a025a9444aa1125b0458816fbb;hp=8de22c1e3c1d4c4c7867cbe24c08b4c6575ef006;hpb=5c10d402b5de7233bc83d7f685b274832e383212;p=helm.git

diff --git a/helm/software/matita/library/nat/times.ma b/helm/software/matita/library/nat/times.ma
index 8de22c1e3..f59622218 100644
--- 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.