Procedural: explicit flavour specification for constants is now working

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

diff --git a/helm/software/matita/contribs/CoRN-Procedural/fta/FTAreg.mma b/helm/software/matita/contribs/CoRN-Procedural/fta/FTAreg.mma
index 58c776f63445af06cf2b67c0a66fb0c0f7718bfc..d96c06c8c3b7258a0a1ec8679613b30f5641c11f 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/fta/FTAreg.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/fta/FTAreg.mma
@@ -81,21 +81,21 @@ inline procedural "cic:/CoRN/fta/FTAreg/Knes_tupp.ind".
 cic:/matita/CoRN-Procedural/fta/FTAreg/Kntup.con
 *)
 
-inline procedural "cic:/CoRN/fta/FTAreg/Knes_fun.con".
+inline procedural "cic:/CoRN/fta/FTAreg/Knes_fun.con" as definition.
 
-inline procedural "cic:/CoRN/fta/FTAreg/Knes_fun_it.con".
+inline procedural "cic:/CoRN/fta/FTAreg/Knes_fun_it.con" as definition.
 
-inline procedural "cic:/CoRN/fta/FTAreg/sK.con".
+inline procedural "cic:/CoRN/fta/FTAreg/sK.con" as definition.
 
-inline procedural "cic:/CoRN/fta/FTAreg/sK_c.con".
+inline procedural "cic:/CoRN/fta/FTAreg/sK_c.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTAreg/sK_c0.con".
+inline procedural "cic:/CoRN/fta/FTAreg/sK_c0.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTAreg/sK_prop1.con".
+inline procedural "cic:/CoRN/fta/FTAreg/sK_prop1.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTAreg/sK_it.con".
+inline procedural "cic:/CoRN/fta/FTAreg/sK_it.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTAreg/sK_prop2.con".
+inline procedural "cic:/CoRN/fta/FTAreg/sK_prop2.con" as lemma.
 
 (* UNEXPORTED
 End Kneser_Sequence
@@ -108,7 +108,7 @@ Section Seq_Exists_Main
 (*#* **Main results
 *)
 
-inline procedural "cic:/CoRN/fta/FTAreg/seq_exists.con".
+inline procedural "cic:/CoRN/fta/FTAreg/seq_exists.con" as lemma.
 
 (* UNEXPORTED
 End Seq_Exists_Main
@@ -138,7 +138,7 @@ alias id "zltc" = "cic:/CoRN/fta/FTAreg/N_Exists/zltc.var".
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/fta/FTAreg/N_Exists/q_.con" "N_Exists__".
+inline procedural "cic:/CoRN/fta/FTAreg/N_Exists/q_.con" "N_Exists__" as definition.
 
 (* end hide *)
 
@@ -146,7 +146,7 @@ alias id "e" = "cic:/CoRN/fta/FTAreg/N_Exists/e.var".
 
 alias id "zlte" = "cic:/CoRN/fta/FTAreg/N_Exists/zlte.var".
 
-inline procedural "cic:/CoRN/fta/FTAreg/N_exists.con".
+inline procedural "cic:/CoRN/fta/FTAreg/N_exists.con" as lemma.
 
 (* UNEXPORTED
 End N_Exists
@@ -183,39 +183,39 @@ alias id "zltc" = "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/zltc.var".
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/q_.con" "Seq_is_CC_CAuchy__".
+inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/q_.con" "Seq_is_CC_CAuchy__" as definition.
 
-inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtq.con" "Seq_is_CC_CAuchy__".
+inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtq.con" "Seq_is_CC_CAuchy__" as definition.
 
-inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtc.con" "Seq_is_CC_CAuchy__".
+inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtc.con" "Seq_is_CC_CAuchy__" as definition.
 
-inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtqlt1.con" "Seq_is_CC_CAuchy__".
+inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtqlt1.con" "Seq_is_CC_CAuchy__" as definition.
 
-inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtq_.con" "Seq_is_CC_CAuchy__".
+inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtq_.con" "Seq_is_CC_CAuchy__" as definition.
 
 (* end hide *)
 
-inline procedural "cic:/CoRN/fta/FTAreg/zlt_nrtq.con".
+inline procedural "cic:/CoRN/fta/FTAreg/zlt_nrtq.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTAreg/zlt_nrtc.con".
+inline procedural "cic:/CoRN/fta/FTAreg/zlt_nrtc.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTAreg/nrt_pow.con".
+inline procedural "cic:/CoRN/fta/FTAreg/nrt_pow.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTAreg/abs_pow_ltRe.con".
+inline procedural "cic:/CoRN/fta/FTAreg/abs_pow_ltRe.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTAreg/abs_pow_ltIm.con".
+inline procedural "cic:/CoRN/fta/FTAreg/abs_pow_ltIm.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTAreg/SublemmaRe.con".
+inline procedural "cic:/CoRN/fta/FTAreg/SublemmaRe.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTAreg/SublemmaIm.con".
+inline procedural "cic:/CoRN/fta/FTAreg/SublemmaIm.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTAreg/seq_is_CC_Cauchy.con".
+inline procedural "cic:/CoRN/fta/FTAreg/seq_is_CC_Cauchy.con" as lemma.
 
 (* UNEXPORTED
 End Seq_is_CC_CAuchy
 *)
 
-inline procedural "cic:/CoRN/fta/FTAreg/FTA_monic.con".
+inline procedural "cic:/CoRN/fta/FTAreg/FTA_monic.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTAreg/FTA_reg.con".
+inline procedural "cic:/CoRN/fta/FTAreg/FTA_reg.con" as lemma.