]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/CoRN-Procedural/ftc/StrongIVT.mma
...
[helm.git] / helm / software / matita / contribs / CoRN-Procedural / ftc / StrongIVT.mma
index 536695ff5b1be050e01fb3057e14246df3d521f2..c964d748fa1d94c6e003cff607f7d74e4fa62afb 100644 (file)
@@ -34,13 +34,21 @@ part, we will simply do that, repeating the previous construction.
 The same notations and conventions apply as before.
 *)
 
-alias id "a" = "cic:/CoRN/ftc/StrongIVT/IVT'/a.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/StrongIVT/IVT'/a.var
+*)
 
-alias id "b" = "cic:/CoRN/ftc/StrongIVT/IVT'/b.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/StrongIVT/IVT'/b.var
+*)
 
-alias id "Hab'" = "cic:/CoRN/ftc/StrongIVT/IVT'/Hab'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/StrongIVT/IVT'/Hab'.var
+*)
 
-alias id "Hab" = "cic:/CoRN/ftc/StrongIVT/IVT'/Hab.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/StrongIVT/IVT'/Hab.var
+*)
 
 (* begin hide *)
 
@@ -50,9 +58,13 @@ inline procedural "cic:/CoRN/ftc/StrongIVT/IVT'/I'.con" "IVT'__" as definition.
 
 (* end hide *)
 
-alias id "F" = "cic:/CoRN/ftc/StrongIVT/IVT'/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/StrongIVT/IVT'/F.var
+*)
 
-alias id "contF" = "cic:/CoRN/ftc/StrongIVT/IVT'/contF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/StrongIVT/IVT'/contF.var
+*)
 
 (* begin hide *)
 
@@ -62,7 +74,9 @@ inline procedural "cic:/CoRN/ftc/StrongIVT/IVT'/incF.con" "IVT'__" as definition
 
 (* begin show *)
 
-alias id "incrF" = "cic:/CoRN/ftc/StrongIVT/IVT'/incrF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/StrongIVT/IVT'/incrF.var
+*)
 
 (* end show *)
 
@@ -78,11 +92,17 @@ inline procedural "cic:/CoRN/ftc/StrongIVT/IVT'/HFab'.con" "IVT'__" as definitio
 
 (* begin show *)
 
-alias id "z" = "cic:/CoRN/ftc/StrongIVT/IVT'/z.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/StrongIVT/IVT'/z.var
+*)
 
-alias id "Haz" = "cic:/CoRN/ftc/StrongIVT/IVT'/Haz.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/StrongIVT/IVT'/Haz.var
+*)
 
-alias id "Hzb" = "cic:/CoRN/ftc/StrongIVT/IVT'/Hzb.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/StrongIVT/IVT'/Hzb.var
+*)
 
 (* end show *)