paramodulation removed

[helm.git] / helm / software / matita / contribs / CoRN-Decl / algebra / CSemiGroups.ma

diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CSemiGroups.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CSemiGroups.ma
index b63dd3175df048d7424ffa43d596363e13088f61..85eac7de25a622f76c81c1da6b2391aa22fcaa0d 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/algebra/CSemiGroups.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CSemiGroups.ma
@@ -16,7 +16,7 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSemiGroups".
 
-include "CoRN_notation.ma".
+include "CoRN.ma".
 
 (* $Id: CSemiGroups.v,v 1.8 2004/04/22 14:49:43 lcf Exp $ *)
 
@@ -37,7 +37,7 @@ inline "cic:/CoRN/algebra/CSemiGroups/is_CSemiGroup.con".
 
 inline "cic:/CoRN/algebra/CSemiGroups/CSemiGroup.ind".
 
-coercion "cic:/matita/CoRN-Decl/algebra/CSemiGroups/csg_crr.con" 0 (* compounds *).
+coercion cic:/matita/CoRN-Decl/algebra/CSemiGroups/csg_crr.con 0 (* compounds *).
 
 (*#*
 %\begin{nameconvention}%
@@ -49,6 +49,10 @@ In the %{\em %names%}% of lemmas, we will denote [[+]] with [plus].
 Implicit Arguments csg_op [c].
 *)
 
+(* NOTATION
+Infix "[+]" := csg_op (at level 50, left associativity).
+*)
+
 (* End_SpecReals *)
 
 (*#* **Semigroup axioms
@@ -156,6 +160,10 @@ End Part_Function_Plus.
 Implicit Arguments Fplus [G].
 *)
 
+(* NOTATION
+Infix "{+}" := Fplus (at level 50, left associativity).
+*)
+
 (* UNEXPORTED
 Hint Resolve included_FPlus : included.
 *)