auto and autogui... some work

[helm.git] / matita / library_auto / auto / nat / le_arith.ma

diff --git a/matita/library_auto/auto/nat/le_arith.ma b/matita/library_auto/auto/nat/le_arith.ma
index ea50a2476204e8b9d301a2eec84533055db205a6..13b4f3ac47153648d70498f3c8f4a543b58af073 100644 (file)
--- a/matita/library_auto/auto/nat/le_arith.ma
+++ b/matita/library_auto/auto/nat/le_arith.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/library_auto/nat/le_arith".
+set "baseuri" "cic:/matita/library_autobatch/nat/le_arith".
 
 include "auto/nat/times.ma".
 include "auto/nat/orders.ma".
@@ -23,7 +23,7 @@ theorem monotonic_le_plus_r:
 simplify.intros.
 elim n;simplify
 [ assumption
-| auto
+| autobatch
   (*apply le_S_S.assumption*)
 ]
 qed.
@@ -47,7 +47,7 @@ theorem monotonic_le_plus_l:
 simplify.intros.
  rewrite < sym_plus.
  rewrite < (sym_plus m).
- auto.
+ autobatch.
 qed.
 *)
 theorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le m + p
@@ -56,7 +56,7 @@ theorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le m + p
 theorem le_plus: \forall n1,n2,m1,m2:nat. n1 \le n2  \to m1 \le m2 
 \to n1 + m1 \le n2 + m2.
 intros.
-auto.
+autobatch.
 (*apply (trans_le ? (n2 + m1)).
 apply le_plus_l.assumption.
 apply le_plus_r.assumption.*)
@@ -65,7 +65,7 @@ qed.
 theorem le_plus_n :\forall n,m:nat. m \le n + m.
 intros.
 change with (O+m \le n+m).
-auto.
+autobatch.
 (*apply le_plus_l.
   apply le_O_n.*)
 qed.
@@ -74,7 +74,7 @@ theorem eq_plus_to_le: \forall n,m,p:nat.n=m+p \to m \le n.
 intros.
 rewrite > H.
 rewrite < sym_plus.
-apply le_plus_n. (* a questo punto funziona anche: auto.*)
+apply le_plus_n. (* a questo punto funziona anche: autobatch.*)
 qed.
 
 (* times *)
@@ -82,7 +82,7 @@ theorem monotonic_le_times_r:
 \forall n:nat.monotonic nat le (\lambda m. n * m).
 simplify.intros.elim n;simplify
 [ apply le_O_n.
-| auto.
+| autobatch.
 (*apply le_plus;
   assumption. *) (* chiudo entrambi i goal attivi in questo modo*)
 ]
@@ -107,7 +107,7 @@ theorem monotonic_le_times_l:
 simplify.intros.
 rewrite < sym_times.
 rewrite < (sym_times m).
-auto.
+autobatch.
 qed.
 *)
 
@@ -117,7 +117,7 @@ theorem le_times_l: \forall p,n,m:nat. n \le m \to n*p \le m*p
 theorem le_times: \forall n1,n2,m1,m2:nat. n1 \le n2  \to m1 \le m2 
 \to n1*m1 \le n2*m2.
 intros.
-auto.
+autobatch.
 (*apply (trans_le ? (n2*m1)).
 apply le_times_l.assumption.
 apply le_times_r.assumption.*)
@@ -125,10 +125,10 @@ qed.
 
 theorem le_times_n: \forall n,m:nat.(S O) \le n \to m \le n*m.
 intros.elim H;simplify
-[ auto
+[ autobatch
   (*elim (plus_n_O ?).
   apply le_n....*)
-| auto
+| autobatch
   (*rewrite < sym_plus.
   apply le_plus_n.*)
 ]