Added a new command "index" for the indexing terms in the "universe".

[helm.git] / matita / contribs / CoRN-Decl / ftc / Rolle.ma

diff --git a/matita/contribs/CoRN-Decl/ftc/Rolle.ma b/matita/contribs/CoRN-Decl/ftc/Rolle.ma
index 21e3b8c34874f1a4f89a401e4bea9189ff9de347..7eda2c5ae097b6ce4dd683ee12bf2b1733d6833f 100644 (file)
--- a/matita/contribs/CoRN-Decl/ftc/Rolle.ma
+++ b/matita/contribs/CoRN-Decl/ftc/Rolle.ma
@@ -112,6 +112,10 @@ inline "cic:/CoRN/ftc/Rolle/incF'.con".
 
 inline "cic:/CoRN/ftc/Rolle/fcp'.con".
 
+(* NOTATION
+Notation cp := (compact_part a b Hab' d Hd).
+*)
+
 inline "cic:/CoRN/ftc/Rolle/Rolle_lemma4.con".
 
 inline "cic:/CoRN/ftc/Rolle/Rolle_lemma5.con".