]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntervals.ma
- setters for data structures now support "commuting conversion"-like
[helm.git] / helm / software / matita / contribs / CoRN-Decl / ftc / MoreIntervals.ma
index bf25f0f7ff0ee94cc8c99ccf55edfdb7fc6de573..30bf4b4231c2c7d5133e3c5279d9c08eb9ad9658 100644 (file)
@@ -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".