Procedural: explicit flavour specification for constants is now working

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / fta / FTA.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/fta/FTA.mma b/helm/software/matita/contribs/CoRN-Procedural/fta/FTA.mma
index acdca7ba045eeda01ac93a029e077abf45cc0285..d8c24667c3452fc4e387fc149bb1a9fe30b43680 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/fta/FTA.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/fta/FTA.mma
@@ -38,7 +38,7 @@ alias id "n" = "cic:/CoRN/fta/FTA/FTA_reg'/n.var".
 
 alias id "f_degree" = "cic:/CoRN/fta/FTA/FTA_reg'/f_degree.var".
 
-inline procedural "cic:/CoRN/fta/FTA/FTA_reg'.con".
+inline procedural "cic:/CoRN/fta/FTA/FTA_reg'.con" as lemma.
 
 (* UNEXPORTED
 End FTA_reg'
@@ -65,15 +65,15 @@ alias id "c" = "cic:/CoRN/fta/FTA/FTA_1/c.var".
 
 alias id "f_c" = "cic:/CoRN/fta/FTA/FTA_1/f_c.var".
 
-inline procedural "cic:/CoRN/fta/FTA/FTA_1a.con".
+inline procedural "cic:/CoRN/fta/FTA/FTA_1a.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTA/FTA_1/g.con" "FTA_1__".
+inline procedural "cic:/CoRN/fta/FTA/FTA_1/g.con" "FTA_1__" as definition.
 
-inline procedural "cic:/CoRN/fta/FTA/FTA_1b.con".
+inline procedural "cic:/CoRN/fta/FTA/FTA_1b.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTA/FTA_1.con".
+inline procedural "cic:/CoRN/fta/FTA/FTA_1.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTA/FTA_1'.con".
+inline procedural "cic:/CoRN/fta/FTA/FTA_1'.con" as lemma.
 
 (* UNEXPORTED
 End FTA_1
@@ -83,11 +83,11 @@ End FTA_1
 Section Fund_Thm_Alg
 *)
 
-inline procedural "cic:/CoRN/fta/FTA/FTA'.con".
+inline procedural "cic:/CoRN/fta/FTA/FTA'.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTA/FTA.con".
+inline procedural "cic:/CoRN/fta/FTA/FTA.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTA/FTA_a_la_Henk.con".
+inline procedural "cic:/CoRN/fta/FTA/FTA_a_la_Henk.con" as lemma.
 
 (* UNEXPORTED
 End Fund_Thm_Alg