- init_cache_and_tables rewritten using the automation_cache

[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 6bbdcec4d2083e0200a3bdb7b431d9d577f00997..87edf468bc958e990d337271656bfaac181756b9 100644 (file)
--- a/helm/software/matita/library/nat/times.ma
+++ b/helm/software/matita/library/nat/times.ma
@@ -129,6 +129,8 @@ variant assoc_times: \forall n,m,p:nat. (n*m)*p = n*(m*p) \def
 associative_times.
 
 lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z).
-intros.autobatch paramodulation.
+intros. 
+demodulate. reflexivity;
+(* autobatch paramodulation. *)
 qed.