X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary_auto%2Fauto%2Fnat%2Fexp.ma;h=69667b7158867a7a97fc8a3f9ae4f6e29c9f792a;hb=a180bddcd4a8f35de3d7292162ba05d0077723aa;hp=f7d1255415e58bde57b049dcbb8e41eaed9da84d;hpb=cf4088e2cabcbce9b112f1e1fd5cfd38fe16d427;p=helm.git

diff --git a/helm/software/matita/library_auto/auto/nat/exp.ma b/helm/software/matita/library_auto/auto/nat/exp.ma
index f7d125541..69667b715 100644
--- a/helm/software/matita/library_auto/auto/nat/exp.ma
+++ b/helm/software/matita/library_auto/auto/nat/exp.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/library_auto/nat/exp".
+set "baseuri" "cic:/matita/library_autobatch/nat/exp".
 
 include "auto/nat/div_and_mod.ma".
 
@@ -21,12 +21,12 @@ let rec exp n m on m\def
  [ O \Rightarrow (S O)
  | (S p) \Rightarrow (times n (exp n p)) ].
 
-interpretation "natural exponent" 'exp a b = (cic:/matita/library_auto/nat/exp/exp.con a b).
+interpretation "natural exponent" 'exp a b = (cic:/matita/library_autobatch/nat/exp/exp.con a b).
 
 theorem exp_plus_times : \forall n,p,q:nat. 
 n \sup (p + q) = (n \sup p) * (n \sup q).
 intros.
-elim p;simplify;auto.
+elim p;simplify;autobatch.
 (*[ rewrite < plus_n_O.
   reflexivity
 | rewrite > H.
@@ -37,14 +37,14 @@ qed.
 
 theorem exp_n_O : \forall n:nat. S O = n \sup O.
 intro.
-auto.
+autobatch.
 (*simplify.
 reflexivity.*)
 qed.
 
 theorem exp_n_SO : \forall n:nat. n = n \sup (S O).
 intro.
-auto.
+autobatch.
 (*simplify.
 rewrite < times_n_SO.
 reflexivity.*)
@@ -54,13 +54,13 @@ theorem exp_exp_times : \forall n,p,q:nat.
 (n \sup p) \sup q = n \sup (p * q).
 intros.
 elim q;simplify
-[ auto.
+[ autobatch.
   (*rewrite < times_n_O.
   simplify.
   reflexivity*)
 | rewrite > H.
   rewrite < exp_plus_times.
-  auto
+  autobatch
   (*rewrite < times_n_Sm.
   reflexivity*)
 ]
@@ -68,7 +68,7 @@ qed.
 
 theorem lt_O_exp: \forall n,m:nat. O < n \to O < n \sup m. 
 intros.
-elim m;simplify;auto.
+elim m;simplify;autobatch.
                 (*unfold lt
 [ apply le_n
 | rewrite > times_n_SO.
@@ -84,11 +84,11 @@ elim m;simplify;unfold lt;
   [ simplify.
     rewrite < plus_n_Sm.    
     apply le_S_S.
-    auto
+    autobatch
     (*apply le_S_S.
     rewrite < sym_plus.
     apply le_plus_n*)
-  | auto
+  | autobatch
     (*apply le_times;assumption*)
   ]
 ]
@@ -100,7 +100,7 @@ intros.
 apply antisym_le
 [ apply le_S_S_to_le.
   rewrite < H1.
-  auto
+  autobatch
   (*change with (m < n \sup m).
   apply lt_m_exp_nm.
   assumption*)
@@ -114,7 +114,7 @@ simplify.
 intros 4.
 apply (nat_elim2 (\lambda x,y.n \sup x = n \sup y \to x = y))
 [ intros.
-  auto
+  autobatch
   (*apply sym_eq.
   apply (exp_to_eq_O n)
   [ assumption
@@ -129,17 +129,17 @@ apply (nat_elim2 (\lambda x,y.n \sup x = n \sup y \to x = y))
   (* esprimere inj_times senza S *)
   cut (\forall a,b:nat.O < n \to n*a=n*b \to a=b)
   [ apply Hcut
-    [ auto
+    [ autobatch
       (*simplify.
       unfold lt.
       apply le_S_S_to_le. 
       apply le_S. 
       assumption*)
-    | (*NB qui auto non chiude il goal, chiuso invece chiamando solo la tattica assumption*)
+    | (*NB qui autobatch non chiude il goal, chiuso invece chiamando solo la tattica assumption*)
       assumption
     ]
   | intros 2.
-    apply (nat_case n);intros;auto
+    apply (nat_case n);intros;autobatch
     (*[ apply False_ind.
       apply (not_le_Sn_O O H3)
     | apply (inj_times_r m1).