X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Procedural%2Ffta%2FFTA.mma;h=d8c24667c3452fc4e387fc149bb1a9fe30b43680;hb=a89360d64f1fcbba917ad743b97a2d973ecf6db2;hp=acdca7ba045eeda01ac93a029e077abf45cc0285;hpb=3e1e59644a24ed855a7f21bf9eab76f96577fd17;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Procedural/fta/FTA.mma b/helm/software/matita/contribs/CoRN-Procedural/fta/FTA.mma
index acdca7ba0..d8c24667c 100644
--- 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