X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FMoreIntervals.ma;h=30bf4b4231c2c7d5133e3c5279d9c08eb9ad9658;hb=55e5bef77f163b29feeb9ad4e83376c5aa301297;hp=bf25f0f7ff0ee94cc8c99ccf55edfdb7fc6de573;hpb=5e01cba364607e7937aec2e359c34f049bb0f108;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntervals.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntervals.ma
index bf25f0f7f..30bf4b423 100644
--- a/helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntervals.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntervals.ma
@@ -216,13 +216,13 @@ such that [P(x)] holds.
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/P.var" "Compact_Constructions__Single_Compact_Interval__".
+alias id "P" = "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/P.var".
 
-inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/wdP.var" "Compact_Constructions__Single_Compact_Interval__".
+alias id "wdP" = "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/wdP.var".
 
-inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/x.var" "Compact_Constructions__Single_Compact_Interval__".
+alias id "x" = "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/x.var".
 
-inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/Hx.var" "Compact_Constructions__Single_Compact_Interval__".
+alias id "Hx" = "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/Hx.var".
 
 inline "cic:/CoRN/ftc/MoreIntervals/compact_single.con".
 
@@ -389,9 +389,9 @@ previously defined concepts.
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/ftc/MoreIntervals/Functions/n.var" "Functions__".
+alias id "n" = "cic:/CoRN/ftc/MoreIntervals/Functions/n.var".
 
-inline "cic:/CoRN/ftc/MoreIntervals/Functions/I.var" "Functions__".
+alias id "I" = "cic:/CoRN/ftc/MoreIntervals/Functions/I.var".
 
 inline "cic:/CoRN/ftc/MoreIntervals/Continuous.con".