Semantic analysis implemented (sort of).

[helm.git] / helm / software / matita / contribs / CoRN-Decl / model / structures / Nsec.ma

diff --git a/helm/software/matita/contribs/CoRN-Decl/model/structures/Nsec.ma b/helm/software/matita/contribs/CoRN-Decl/model/structures/Nsec.ma
index 82d341b2748b894a5a3214119dc005405826b661..084be106ca29f4028954570baeb35b57b5480354 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/model/structures/Nsec.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/model/structures/Nsec.ma
@@ -39,6 +39,10 @@ inline "cic:/CoRN/model/structures/Nsec/S_O.con".
 
 inline "cic:/CoRN/model/structures/Nsec/ap_nat.con".
 
+(* NOTATION
+Infix "{#N}" := ap_nat (no associativity, at level 90).
+*)
+
 inline "cic:/CoRN/model/structures/Nsec/ap_nat_irreflexive0.con".
 
 inline "cic:/CoRN/model/structures/Nsec/ap_nat_symmetric0.con".