X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCRings.ma;h=4a79f1220547c3a11e19d8aaab83e0626a2bd050;hb=946be00a2b9e1713e934414bd8419f267cca1077;hp=9210cad60b7c2cd6bc6ecd79f79592719f9921fa;hpb=94873bb61a663b4fca3dc6d07b7bb9f42122003e;p=helm.git

diff --git a/matita/contribs/CoRN-Decl/algebra/CRings.ma b/matita/contribs/CoRN-Decl/algebra/CRings.ma
index 9210cad60..4a79f1220 100644
--- a/matita/contribs/CoRN-Decl/algebra/CRings.ma
+++ b/matita/contribs/CoRN-Decl/algebra/CRings.ma
@@ -16,7 +16,7 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/algebra/CRings".
 
-include "CoRN_notation.ma".
+include "CoRN.ma".
 
 (* $Id: CRings.v,v 1.8 2004/04/23 10:00:53 lcf Exp $ *)
 
@@ -83,7 +83,7 @@ inline "cic:/CoRN/algebra/CRings/is_CRing.ind".
 
 inline "cic:/CoRN/algebra/CRings/CRing.ind".
 
-coercion "cic:/matita/CoRN-Decl/algebra/CRings/cr_crr.con" 0 (* compounds *).
+coercion cic:/matita/CoRN-Decl/algebra/CRings/cr_crr.con 0 (* compounds *).
 
 inline "cic:/CoRN/algebra/CRings/cr_plus.con".
 
@@ -91,6 +91,10 @@ inline "cic:/CoRN/algebra/CRings/cr_inv.con".
 
 inline "cic:/CoRN/algebra/CRings/cr_minus.con".
 
+(* NOTATION
+Notation One := (cr_one _).
+*)
+
 (* End_SpecReals *)
 
 (* Begin_SpecReals *)
@@ -106,6 +110,10 @@ and [[*]] with [mult].
 Implicit Arguments cr_mult [c].
 *)
 
+(* NOTATION
+Infix "[*]" := cr_mult (at level 40, left associativity).
+*)
+
 (* UNEXPORTED
 Section CRing_axioms.
 *)
@@ -356,6 +364,10 @@ End exponentiation.
 
 (* End_SpecReals *)
 
+(* NOTATION
+Notation "x [^] n" := (nexp_op _ n x) (at level 20).
+*)
+
 (* UNEXPORTED
 Implicit Arguments nexp_op [R].
 *)
@@ -410,6 +422,50 @@ Implicit Arguments nring [R].
 
 (* End_SpecReals *)
 
+(* NOTATION
+Notation Two := (nring 2).
+*)
+
+(* NOTATION
+Notation Three := (nring 3).
+*)
+
+(* NOTATION
+Notation Four := (nring 4).
+*)
+
+(* NOTATION
+Notation Six := (nring 6).
+*)
+
+(* NOTATION
+Notation Eight := (nring 8).
+*)
+
+(* NOTATION
+Notation Twelve := (nring 12).
+*)
+
+(* NOTATION
+Notation Sixteen := (nring 16).
+*)
+
+(* NOTATION
+Notation Nine := (nring 9).
+*)
+
+(* NOTATION
+Notation Eighteen := (nring 18).
+*)
+
+(* NOTATION
+Notation TwentyFour := (nring 24).
+*)
+
+(* NOTATION
+Notation FortyEight := (nring 48).
+*)
+
 inline "cic:/CoRN/algebra/CRings/one_plus_one.con".
 
 inline "cic:/CoRN/algebra/CRings/x_plus_x.con".
@@ -902,14 +958,26 @@ inline "cic:/CoRN/algebra/CRings/Fscalmult.con".
 Implicit Arguments Fmult [R].
 *)
 
+(* NOTATION
+Infix "{*}" := Fmult (at level 40, left associativity).
+*)
+
 (* UNEXPORTED
 Implicit Arguments Fscalmult [R].
 *)
 
+(* NOTATION
+Infix "{**}" := Fscalmult (at level 40, left associativity).
+*)
+
 (* UNEXPORTED
 Implicit Arguments Fnth [R].
 *)
 
+(* NOTATION
+Infix "{^}" := Fnth (at level 30, right associativity).
+*)
+
 (* UNEXPORTED
 Section ScalarMultiplication.
 *)