auto ==> autobatch

Two kind of failures still there:
 1) fails to find a proof
 2) finds a proof, but the proof does not type-check

diff --git a/helm/software/matita/tests/paramodulation/irratsqrt2.ma b/helm/software/matita/tests/paramodulation/irratsqrt2.ma
index b19984d7dfa214912573ba013d85361dff4f99ad..5c976bcb9f3f04a3326f1bef2c0759af7f60ea0f 100644 (file)
--- a/helm/software/matita/tests/paramodulation/irratsqrt2.ma
+++ b/helm/software/matita/tests/paramodulation/irratsqrt2.ma
@@ -25,14 +25,14 @@ theorem prova :
   \forall H1: \forall x.P x \to O = x.
    O = S (S (S (S (S O)))).
    intros.
-   auto new.
+   autobatch.
  qed.
  
 theorem example2:
 \forall x: nat. (x+S O)*(x-S O) = x*x - S O.
 intro;
 apply (nat_case x);
- [ auto new timeout = 1.|intro.auto new timeout = 1.]
+ [ autobatch timeout = 1.|intro.autobatch timeout = 1.]
 qed.
 
 theorem irratsqrt2_byhand:
@@ -55,7 +55,7 @@ theorem irratsqrt2_byhand:
   two = o.
   intros.
   cut (divides two a);
-    [2:elim (H8 a a);[assumption.|assumption|rewrite > H9.auto new.]
+    [2:elim (H8 a a);[assumption.|assumption|rewrite > H9.autobatch.]
     |elim (H6 ? ? Hcut).
      cut (divides two b);
        [ apply (H10 ? Hcut Hcut1).
@@ -89,7 +89,7 @@ theorem irratsqrt2_byhand':
   two = o.
   intros.
   cut (divides two a);
-    [2:elim (H8 a a);[assumption.|assumption|rewrite > H9.auto new.]
+    [2:elim (H8 a a);[assumption.|assumption|rewrite > H9.autobatch.]
     |(*elim (H6 ? ? Hcut). *)
      cut (divides two b);
        [ apply (H10 ? Hcut Hcut1).
@@ -126,7 +126,7 @@ theorem irratsqrt2:
   \forall H6:\forall x.divides x a \to divides x b \to x = o.
   two = o.
 intros.
-auto new depth = 5 timeout = 180.
+autobatch depth = 5 timeout = 180.
 qed.
 
 (* time: 146s *)
@@ -136,19 +136,19 @@ qed.
 
   cut (divides two a);[|
     (* apply H8;apply (H7 two (m a a) (m b b));symmetry;assumption. *)
-    auto new depth = 4 width = 3 use_paramod = false. ]
-  (*auto new depth = 5.*)
+    autobatch depth = 4 width = 3 use_paramod = false. ]
+  (*autobatch depth = 5.*)
   
   apply H10;
   [ assumption.
-  |(*auto new depth = 4.*) apply H8;   
-         (*auto new.*)
+  |(*autobatch depth = 4.*) apply H8;   
+         (*autobatch.*)
          apply (H7 ? ? (m (f two a) (f two a)));
          apply (H5 two ? ?);
          cut ((\lambda x:A.m x (m two ?)=m x (m b b))?);
          [|||simplify;
-         auto paramodulation.
-         (*auto new.*)
+         autobatch paramodulation.
+         (*autobatch new.*)
          rewrite < H9.
          rewrite < (H6 two a Hcut) in \vdash (? ? ? %).
          rewrite < H2.apply eq_f.