X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Falgebra%2FCoRN%2FSemiGroups.ma;h=b57d3b2fde5f22d2a735e277df8be2f35090d085;hb=9e291b4d0a99118cd0a1c5540ef00c25ca37a56d;hp=3d209099bd36a4792e274b7b878a6404f1d8c88c;hpb=0070f04a500ec6e12dc063ff5acb8a7622b51283;p=helm.git

diff --git a/helm/software/matita/library/algebra/CoRN/SemiGroups.ma b/helm/software/matita/library/algebra/CoRN/SemiGroups.ma
index 3d209099b..b57d3b2fd 100644
--- a/helm/software/matita/library/algebra/CoRN/SemiGroups.ma
+++ b/helm/software/matita/library/algebra/CoRN/SemiGroups.ma
@@ -136,7 +136,7 @@ intros (H2 H3).
 elim (H1 e) 0.
 clear H1.
 intros (H4 H5).
-auto new.
+autobatch new.
 qed.
 (*
 astepr (e[+]f). 
@@ -155,7 +155,7 @@ We can also define a similar addition operator, which will be denoted by [{+}],
 %\begin{convention}% Whenever possible, we will denote the functional construction corresponding to an algebraic operation by the same symbol enclosed in curly braces.
 %\end{convention}%
 
-At this stage, we will always consider automorphisms; we %{\em %could%}% treat this in a more general setting, but we feel that it wouldn't really be a useful effort.
+At this stage, we will always consider autobatchmorphisms; we %{\em %could%}% treat this in a more general setting, but we feel that it wouldn't really be a useful effort.
 
 %\begin{convention}% Let [G:CSemiGroup] and [F,F':(PartFunct G)] and denote by [P] and [Q], respectively, the predicates characterizing their domains.
 %\end{convention}%
@@ -269,10 +269,10 @@ definition dprod: \forall M1,M2:CSemiGroup. \forall x:ProdCSetoid (csg_crr M1) (
   \lambda M1,M2:CSemiGroup. \lambda x:ProdCSetoid (csg_crr M1) (csg_crr M2).
   \lambda y:ProdCSetoid (csg_crr M1) (csg_crr M2).
   match x with 
-    [pairT (x1: (cs_crr (csg_crr M1))) (x2: (cs_crr (csg_crr M2))) \Rightarrow 
+    [pair (x1: (cs_crr (csg_crr M1))) (x2: (cs_crr (csg_crr M2))) \Rightarrow 
      match y with 
-       [pairT (y1: (cs_crr (csg_crr M1))) (y2: (cs_crr (csg_crr M2))) \Rightarrow 
-          pairT (cs_crr (csg_crr M1)) (cs_crr (csg_crr M2))
+       [pair (y1: (cs_crr (csg_crr M1))) (y2: (cs_crr (csg_crr M2))) \Rightarrow 
+          pair (cs_crr (csg_crr M1)) (cs_crr (csg_crr M2))
 (csbf_fun ? ? ? (csg_op M1) x1 y1) (csbf_fun ? ? ? (csg_op M2) x2 y2)]].
 
 lemma dprod_strext: \forall M1,M2:CSemiGroup.