]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/CoRN-Procedural/ftc/COrdLemmas.mma
...
[helm.git] / helm / software / matita / contribs / CoRN-Procedural / ftc / COrdLemmas.mma
index 51b18daa061329aede2f058afa37d440f17bdcf9..83b34c71577a133ce62b103dc69781ec3138548b 100644 (file)
@@ -37,7 +37,9 @@ the proof that any two partitions with no common point have a common
 refinement).
 *)
 
-alias id "F" = "cic:/CoRN/ftc/COrdLemmas/Lemmas/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/COrdLemmas/Lemmas/F.var
+*)
 
 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_lt.con" as lemma.
 
@@ -63,13 +65,21 @@ inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_4d.con" as lemma.
 
 (* begin hide *)
 
-alias id "f" = "cic:/CoRN/ftc/COrdLemmas/Lemmas/f.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/COrdLemmas/Lemmas/f.var
+*)
 
-alias id "f0" = "cic:/CoRN/ftc/COrdLemmas/Lemmas/f0.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/COrdLemmas/Lemmas/f0.var
+*)
 
-alias id "f_mon" = "cic:/CoRN/ftc/COrdLemmas/Lemmas/f_mon.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/COrdLemmas/Lemmas/f_mon.var
+*)
 
-alias id "h" = "cic:/CoRN/ftc/COrdLemmas/Lemmas/h.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/COrdLemmas/Lemmas/h.var
+*)
 
 (* end hide *)
 
@@ -105,7 +115,9 @@ inline procedural "cic:/CoRN/ftc/COrdLemmas/More_Lemmas/f'.con" "More_Lemmas__"
 
 (* end hide *)
 
-alias id "F" = "cic:/CoRN/ftc/COrdLemmas/More_Lemmas/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/COrdLemmas/More_Lemmas/F.var
+*)
 
 (* begin show *)