X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary_auto%2Fauto%2Fnat%2Fplus.ma;h=59259ca68ff5b5517e9ca0391c7b7a702e0978ef;hb=c78a913e4e45c1128b59ca8be9d53fc0c36fc9e0;hp=02b819f46fcfcac850b9b19f6bded25ac776ae39;hpb=797f9ece92237a8d583a0c32ef4fa755299f9949;p=helm.git

diff --git a/helm/software/matita/library_auto/auto/nat/plus.ma b/helm/software/matita/library_auto/auto/nat/plus.ma
index 02b819f46..59259ca68 100644
--- a/helm/software/matita/library_auto/auto/nat/plus.ma
+++ b/helm/software/matita/library_auto/auto/nat/plus.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/library_auto/nat/plus".
+set "baseuri" "cic:/matita/library_autobatch/nat/plus".
 
 include "auto/nat/nat.ma".
 
@@ -22,14 +22,14 @@ let rec plus n m \def
  | (S p) \Rightarrow S (plus p m) ].
 
 (*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural plus" 'plus x y = (cic:/matita/library_auto/nat/plus/plus.con x y).
+interpretation "natural plus" 'plus x y = (cic:/matita/library_autobatch/nat/plus/plus.con x y).
 
 theorem plus_n_O: \forall n:nat. n = n+O.
 intros.elim n
-[ auto
+[ autobatch
   (*simplify.
   reflexivity*)
-| auto
+| autobatch
   (*simplify.
   apply eq_f.
   assumption.*)
@@ -38,11 +38,11 @@ qed.
 
 theorem plus_n_Sm : \forall n,m:nat. S (n+m) = n+(S m).
 intros.elim n
-[ auto
+[ autobatch
   (*simplify.
   reflexivity.*)
 | simplify.
-  auto
+  autobatch
   (*
   apply eq_f.
   assumption.*)]
@@ -50,22 +50,22 @@ qed.
 
 theorem sym_plus: \forall n,m:nat. n+m = m+n.
 intros.elim n
-[ auto
+[ autobatch
   (*simplify.
   apply plus_n_O.*)
 | simplify.
-  auto
+  autobatch
   (*rewrite > H.
   apply plus_n_Sm.*)]
 qed.
 
 theorem associative_plus : associative nat plus.
 unfold associative.intros.elim x
-[auto
+[autobatch
  (*simplify.
  reflexivity.*)
 |simplify.
- auto
+ autobatch
  (*apply eq_f.
  assumption.*)
 ]
@@ -77,7 +77,7 @@ theorem assoc_plus : \forall n,m,p:nat. (n+m)+p = n+(m+p)
 theorem injective_plus_r: \forall n:nat.injective nat nat (\lambda m.n+m).
 intro.simplify.intros 2.elim n
 [ exact H
-| auto
+| autobatch
   (*apply H.apply inj_S.apply H1.*)
 ]
 qed.
@@ -86,7 +86,7 @@ theorem inj_plus_r: \forall p,n,m:nat. p+n = p+m \to n=m
 \def injective_plus_r.
 
 theorem injective_plus_l: \forall m:nat.injective nat nat (\lambda n.n+m).
-intro.simplify.intros.auto.
+intro.simplify.intros.autobatch.
 (*apply (injective_plus_r m).
 rewrite < sym_plus.
 rewrite < (sym_plus y).