auto --> autobatch

diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma b/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma
index 288e0626d82cf7545b9cb3e277d21c614264ee5e..44823fc814b685f673bb1665b1a238e195c842c8 100644 (file)
--- a/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma
+++ b/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma
@@ -102,9 +102,9 @@ theorem trans_eq : \forall A:Type. \forall x,y,z:A. x=y \to y=z \to x=z.
 qed.
 
 theorem plus_reg_l: \forall n,m,p. n + m = n + p \to m = p.
- intros. apply plus_reg_l; auto.
+ intros. apply plus_reg_l; autobatch.
 qed.
 
 theorem plus_le_reg_l: \forall p,n,m. p + n <= p + m \to n <= m.
- intros. apply plus_le_reg_l; auto.
+ intros. apply plus_le_reg_l; autobatch.
 qed.

diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma
index 3a48e5987353aeff75e5ecf626b95bf92c723ec7..b39e419ad6dc0d5fa2fd8553e54f556faeb9d58d 100644 (file)
--- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma
+++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma
@@ -21,7 +21,7 @@ include "Lift/defs.ma".
 theorem lift_inv_sort_1: \forall l, i, h, x.
                          Lift l i (sort h) x \to
                          x = sort h.
- intros. inversion H; clear H; intros; subst. auto.
+ intros. inversion H; clear H; intros; subst. autobatch.
 qed.
 
 theorem lift_inv_lref_1: \forall l, i, j1, x.
@@ -54,7 +54,7 @@ qed.
 theorem lift_inv_sort_2: \forall l, i, x, h.
                          Lift l i x (sort h) \to
                          x = sort h.
- intros. inversion H; clear H; intros; subst. auto.
+ intros. inversion H; clear H; intros; subst. autobatch.
 qed.
 
 theorem lift_inv_lref_2: \forall l, i, x, j2.

diff --git a/matita/contribs/RELATIONAL/NLE/inv.ma b/matita/contribs/RELATIONAL/NLE/inv.ma
index 54ab40ae776adbb6e0166678d452da575429dfbc..0007f3bc1f76989346485889092f6831c3631434 100644 (file)
--- a/matita/contribs/RELATIONAL/NLE/inv.ma
+++ b/matita/contribs/RELATIONAL/NLE/inv.ma
@@ -18,11 +18,11 @@ include "NLE/defs.ma".
 
 theorem nle_inv_succ_1: \forall x,y. x < y \to 
                         \exists z. y = succ z \land x <= z.
- intros. inversion H; clear H; intros; subst. auto.
+ intros. inversion H; clear H; intros; subst. autobatch.
 qed.
 
 theorem nle_inv_succ_succ: \forall x,y. x < succ y \to x <= y.
- intros. inversion H; clear H; intros; subst. auto.
+ intros. inversion H; clear H; intros; subst. autobatch.
 qed.
 
 theorem nle_inv_succ_zero: \forall x. x < zero \to False.
@@ -30,7 +30,7 @@ theorem nle_inv_succ_zero: \forall x. x < zero \to False.
 qed.
 
 theorem nle_inv_zero_2: \forall x. x <= zero \to x = zero.
- intros. inversion H; clear H; intros; subst. auto.
+ intros. inversion H; clear H; intros; subst. autobatch.
 qed.
 
 theorem nle_inv_succ_2: \forall y,x. x <= succ y \to

diff --git a/matita/contribs/RELATIONAL/NLE/nplus.ma b/matita/contribs/RELATIONAL/NLE/nplus.ma
index 78ca2e569f90fbb3e0f9b19f79cb97d7be547b1f..d90adb92627ddcc8bdb08c939b30d8a802bb3421 100644 (file)
--- a/matita/contribs/RELATIONAL/NLE/nplus.ma
+++ b/matita/contribs/RELATIONAL/NLE/nplus.ma
@@ -17,7 +17,7 @@ set "baseuri" "cic:/matita/RELATIONAL/NLE/nplus".
 include "NLE/defs.ma".
 
 theorem nle_nplus: \forall p, q, r. (p + q == r) \to q <= r.
- intros. elim H; clear H q r; auto.
+ intros. elim H; clear H q r; autobatch.
 qed.
 
 axiom nle_nplus_comp: \forall x1, x2, x3. (x1 + x2 == x3) \to

diff --git a/matita/contribs/RELATIONAL/NPlus/inv.ma b/matita/contribs/RELATIONAL/NPlus/inv.ma
index ae1d4787071f27582fc77a47932ce9211d97154b..5299d5790debc2eacbbd83b5aea99cdc09e69e4f 100644 (file)
--- a/matita/contribs/RELATIONAL/NPlus/inv.ma
+++ b/matita/contribs/RELATIONAL/NPlus/inv.ma
@@ -19,7 +19,7 @@ include "NPlus/defs.ma".
 (* Inversion lemmas *********************************************************)
 
 theorem nplus_inv_zero_1: \forall q,r. (zero + q == r) \to q = r.
- intros. elim H; clear H q r; auto.
+ intros. elim H; clear H q r; autobatch.
 qed.
 
 theorem nplus_inv_succ_1: \forall p,q,r. ((succ p) + q == r) \to 
@@ -31,7 +31,7 @@ theorem nplus_inv_succ_1: \forall p,q,r. ((succ p) + q == r) \to
 qed.
 
 theorem nplus_inv_zero_2: \forall p,r. (p + zero == r) \to p = r.
- intros. inversion H; clear H; intros; subst. auto.
+ intros. inversion H; clear H; intros; subst. autobatch.
 qed.
 
 theorem nplus_inv_succ_2: \forall p,q,r. (p + (succ q) == r) \to 
@@ -41,7 +41,7 @@ qed.
 
 theorem nplus_inv_zero_3: \forall p,q. (p + q == zero) \to 
                           p = zero \land q = zero.
- intros. inversion H; clear H; intros; subst. auto.
+ intros. inversion H; clear H; intros; subst. autobatch.
 qed.
 
 theorem nplus_inv_succ_3: \forall p,q,r. (p + q == (succ r)) \to
@@ -55,25 +55,25 @@ qed.
 theorem nplus_inv_succ_2_3: \forall p,q,r.
                             (p + (succ q) == (succ r)) \to p + q == r.
  intros. 
- lapply linear nplus_inv_succ_2 to H. decompose. subst. auto.
+ lapply linear nplus_inv_succ_2 to H. decompose. subst. autobatch.
 qed.
 
 theorem nplus_inv_succ_1_3: \forall p,q,r.
                             ((succ p) + q == (succ r)) \to p + q == r.
  intros. 
- lapply linear nplus_inv_succ_1 to H. decompose. subst. auto.
+ lapply linear nplus_inv_succ_1 to H. decompose. subst. autobatch.
 qed.
 
 theorem nplus_inv_eq_2_3: \forall p,q. (p + q == q) \to p = zero.
  intros 2. elim q; clear q;
  [ lapply linear nplus_inv_zero_2 to H
  | lapply linear nplus_inv_succ_2_3 to H1
- ]; auto.
+ ]; autobatch.
 qed.
 
 theorem nplus_inv_eq_1_3: \forall p,q. (p + q == p) \to q = zero.
  intros 1. elim p; clear p;
  [ lapply linear nplus_inv_zero_1 to H
  | lapply linear nplus_inv_succ_1_3 to H1.
- ]; auto.
+ ]; autobatch.
 qed.

diff --git a/matita/dama/ordered_sets.ma b/matita/dama/ordered_sets.ma
index 1ca191339b697514c39b171ed9111ef8c6a1003c..62b9348659674a35114f6213157f2c20573ad552 100644 (file)
--- a/matita/dama/ordered_sets.ma
+++ b/matita/dama/ordered_sets.ma
@@ -330,7 +330,7 @@ theorem tail_inf_increasing:
       assumption
     | unfold y;
       simplify;
-      auto paramodulation library
+      autobatch paramodulation library
     ]
  ].
 qed.

diff --git a/matita/tests/fguidi.ma b/matita/tests/fguidi.ma
index 5def3ec470f664e0ac00c32e1d0c49a97b81d697..165f9ce302fd35e0c2aaa9776bfe652f3996484b 100644 (file)
--- a/matita/tests/fguidi.ma
+++ b/matita/tests/fguidi.ma
@@ -84,8 +84,8 @@ theorem le_gen_S_x_aux: \forall m,x,y. (le y x) \to (y = S m) \to
 intros 4. elim H; clear H x y.
 apply eq_gen_S_O. exact m. elim H1. auto paramodulation.
 clear H2. cut (n = m).
-elim Hcut. apply ex_intro. exact n1. split; auto.
-apply eq_gen_S_S. auto.
+elim Hcut. apply ex_intro. exact n1. split; autobatch.
+apply eq_gen_S_S. autobatch.
 qed.
 
 theorem le_gen_S_x: \forall m,x. (le (S m) x) \to