X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Ford.ma;h=4fd2fd2828bdd75616596a093d6f063339bd004c;hb=e65e31bab82994cf8400bb4c294cf7d16fa2c83c;hp=c45bfe701df66faeb665c9296c2e31690f609ff6;hpb=06a19bec47845ecffe3bf9d9a95d3d4dadf76861;p=helm.git

diff --git a/helm/software/matita/library/nat/ord.ma b/helm/software/matita/library/nat/ord.ma
index c45bfe701..4fd2fd282 100644
--- a/helm/software/matita/library/nat/ord.ma
+++ b/helm/software/matita/library/nat/ord.ma
@@ -17,7 +17,7 @@ set "baseuri" "cic:/matita/nat/ord".
 include "datatypes/constructors.ma".
 include "nat/exp.ma".
 include "nat/gcd.ma".
-include "nat/relevant_equations.ma". (* required by auto paramod *)
+include "nat/relevant_equations.ma". (* required by autobatch paramod *)
 
 let rec p_ord_aux p n m \def
   match n \mod m with
@@ -213,7 +213,7 @@ apply (absurd ? ? H10 H5).
 apply (absurd ? ? H10 H7).
 (* rewrite > H6.
 rewrite > H8. *)
-auto paramodulation.
+autobatch paramodulation.
 unfold prime in H. elim H. assumption.
 qed.
 
@@ -259,7 +259,7 @@ cut (S O < p)
          apply (lt_to_not_eq O ? H).
          rewrite > H7.
          rewrite < H10.
-         auto
+         autobatch
         ]
       |elim c
         [rewrite > sym_gcd.
@@ -270,7 +270,7 @@ cut (S O < p)
           |apply lt_O_exp.apply lt_to_le.assumption
           |rewrite > sym_gcd.
            (* hint non trova prime_to_gcd_SO e
-              auto non chiude il goal *)
+              autobatch non chiude il goal *)
            apply prime_to_gcd_SO
             [assumption|assumption]
           |assumption
@@ -297,7 +297,7 @@ cut (S O < p)
               |apply lt_O_exp.apply lt_to_le.assumption
               |rewrite > sym_gcd.
               (* hint non trova prime_to_gcd_SO e
-                 auto non chiude il goal *)
+                 autobatch non chiude il goal *)
                apply prime_to_gcd_SO
                 [assumption|assumption]
               |rewrite > sym_gcd. assumption