From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 26 May 2009 10:47:42 +0000 (+0000)
Subject: removed a call to autobatch.
X-Git-Tag: make_still_working~3947
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9be9ca06b0050a29f0d5611c2d3254125557e59d;p=helm.git

removed a call to autobatch.
---

diff --git a/helm/software/matita/library/Z/moebius.ma b/helm/software/matita/library/Z/moebius.ma
index b9d12c223..14f2b65e7 100644
--- a/helm/software/matita/library/Z/moebius.ma
+++ b/helm/software/matita/library/Z/moebius.ma
@@ -348,7 +348,11 @@ lapply (exp_ord (nth_prime (max_prime_factor n)) n)
           (ord_rem n (nth_prime (max_prime_factor n))))
           [apply lt_to_le.assumption
           |apply le_n
-          |autobatch
+          |apply sym_eq.
+           apply p_ord_exp1.apply lt_O_nth_prime_n.
+           apply not_divides_ord_rem.apply lt_S_to_lt. apply H.
+           apply lt_SO_nth_prime_n.rewrite > sym_times.rewrite < Hletin.
+           reflexivity.
           |assumption
           ]
         |left.apply sym_eq.assumption