X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Fftc%2FRolle.ma;h=7eda2c5ae097b6ce4dd683ee12bf2b1733d6833f;hb=666e2a3fcbfffd2df99650e3404965e95e6b352b;hp=21e3b8c34874f1a4f89a401e4bea9189ff9de347;hpb=f104e234238586ac846881feb30e1b56a509cfd3;p=helm.git

diff --git a/matita/contribs/CoRN-Decl/ftc/Rolle.ma b/matita/contribs/CoRN-Decl/ftc/Rolle.ma
index 21e3b8c34..7eda2c5ae 100644
--- 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".