Procedural: explicit flavour specification for constants is now working

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / reals / R_morphism.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/reals/R_morphism.mma b/helm/software/matita/contribs/CoRN-Procedural/reals/R_morphism.mma
index ac45467d8762f00dcc2099bae6e815f680fd7181..1483e41047ad5a4f69fbfa402c00b512218e7b50 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/reals/R_morphism.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/reals/R_morphism.mma
@@ -26,7 +26,7 @@ include "reals/CReals.ma".
 
 (* This comes from CReals1.v *)
 
-inline procedural "cic:/CoRN/reals/R_morphism/Cauchy_Lim_prop2.con".
+inline procedural "cic:/CoRN/reals/R_morphism/Cauchy_Lim_prop2.con" as definition.
 
 (* UNEXPORTED
 Section morphism
@@ -54,18 +54,18 @@ alias id "g1" = "cic:/CoRN/reals/R_morphism/morphism/morphism_details/g1.var".
 
 alias id "g2" = "cic:/CoRN/reals/R_morphism/morphism/morphism_details/g2.var".
 
-inline procedural "cic:/CoRN/reals/R_morphism/fun_pres_relation.con".
+inline procedural "cic:/CoRN/reals/R_morphism/fun_pres_relation.con" as definition.
 
-inline procedural "cic:/CoRN/reals/R_morphism/fun_pres_un_fun.con".
+inline procedural "cic:/CoRN/reals/R_morphism/fun_pres_un_fun.con" as definition.
 
-inline procedural "cic:/CoRN/reals/R_morphism/fun_pres_bin_fun.con".
+inline procedural "cic:/CoRN/reals/R_morphism/fun_pres_bin_fun.con" as definition.
 
 (*
 Definition fun_pres_partial_fun:=(x:R1;H1:x[#]Zero;H2:(phi x)[#]Zero)
 (phi (nzinj R1 (i1 (nzpro R1 x H1))))[=](nzinj R2 (i2 (nzpro R2 (phi x) H2))).
 *)
 
-inline procedural "cic:/CoRN/reals/R_morphism/fun_pres_Lim.con".
+inline procedural "cic:/CoRN/reals/R_morphism/fun_pres_Lim.con" as definition.
 
 (* UNEXPORTED
 End morphism_details
@@ -86,39 +86,39 @@ Definition Homo_as_CSetoid_fun:=
           ).
 *****************)
 
-inline procedural "cic:/CoRN/reals/R_morphism/map_strext_unfolded.con".
+inline procedural "cic:/CoRN/reals/R_morphism/map_strext_unfolded.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/R_morphism/map_wd_unfolded.con".
+inline procedural "cic:/CoRN/reals/R_morphism/map_wd_unfolded.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/R_morphism/map_pres_less_unfolded.con".
+inline procedural "cic:/CoRN/reals/R_morphism/map_pres_less_unfolded.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/R_morphism/map_pres_plus_unfolded.con".
+inline procedural "cic:/CoRN/reals/R_morphism/map_pres_plus_unfolded.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/R_morphism/map_pres_mult_unfolded.con".
+inline procedural "cic:/CoRN/reals/R_morphism/map_pres_mult_unfolded.con" as lemma.
 
 (* Now we start to derive some useful properties of a Homomorphism *)
 
-inline procedural "cic:/CoRN/reals/R_morphism/map_pres_zero.con".
+inline procedural "cic:/CoRN/reals/R_morphism/map_pres_zero.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/R_morphism/map_pres_zero_unfolded.con".
+inline procedural "cic:/CoRN/reals/R_morphism/map_pres_zero_unfolded.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/R_morphism/map_pres_minus.con".
+inline procedural "cic:/CoRN/reals/R_morphism/map_pres_minus.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/R_morphism/map_pres_minus_unfolded.con".
+inline procedural "cic:/CoRN/reals/R_morphism/map_pres_minus_unfolded.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/R_morphism/map_pres_apartness.con".
+inline procedural "cic:/CoRN/reals/R_morphism/map_pres_apartness.con" as lemma.
 
 (* Merely a useful special case *)
 
-inline procedural "cic:/CoRN/reals/R_morphism/map_pres_ap_zero.con".
+inline procedural "cic:/CoRN/reals/R_morphism/map_pres_ap_zero.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/R_morphism/map_pres_one.con".
+inline procedural "cic:/CoRN/reals/R_morphism/map_pres_one.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/R_morphism/map_pres_one_unfolded.con".
+inline procedural "cic:/CoRN/reals/R_morphism/map_pres_one_unfolded.con" as lemma.
 
 (* I will not use the following lemma *)
 
-inline procedural "cic:/CoRN/reals/R_morphism/map_pres_inv_unfolded.con".
+inline procedural "cic:/CoRN/reals/R_morphism/map_pres_inv_unfolded.con" as lemma.
 
 (* UNEXPORTED
 End morphism
@@ -138,19 +138,19 @@ alias id "f" = "cic:/CoRN/reals/R_morphism/composition/f.var".
 
 alias id "g" = "cic:/CoRN/reals/R_morphism/composition/g.var".
 
-inline procedural "cic:/CoRN/reals/R_morphism/compose.con".
+inline procedural "cic:/CoRN/reals/R_morphism/compose.con" as definition.
 
-inline procedural "cic:/CoRN/reals/R_morphism/compose_strext.con".
+inline procedural "cic:/CoRN/reals/R_morphism/compose_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/R_morphism/compose_pres_less.con".
+inline procedural "cic:/CoRN/reals/R_morphism/compose_pres_less.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/R_morphism/compose_pres_plus.con".
+inline procedural "cic:/CoRN/reals/R_morphism/compose_pres_plus.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/R_morphism/compose_pres_mult.con".
+inline procedural "cic:/CoRN/reals/R_morphism/compose_pres_mult.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/R_morphism/compose_pres_Lim.con".
+inline procedural "cic:/CoRN/reals/R_morphism/compose_pres_Lim.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/R_morphism/Compose.con".
+inline procedural "cic:/CoRN/reals/R_morphism/Compose.con" as definition.
 
 (* UNEXPORTED
 End composition
@@ -172,7 +172,7 @@ alias id "R3" = "cic:/CoRN/reals/R_morphism/isomorphism/identity_map/R3.var".
 
 alias id "f" = "cic:/CoRN/reals/R_morphism/isomorphism/identity_map/f.var".
 
-inline procedural "cic:/CoRN/reals/R_morphism/map_is_id.con".
+inline procedural "cic:/CoRN/reals/R_morphism/map_is_id.con" as definition.
 
 (* UNEXPORTED
 End identity_map
@@ -194,7 +194,7 @@ alias id "R2" = "cic:/CoRN/reals/R_morphism/surjective_map/R2.var".
 
 alias id "f" = "cic:/CoRN/reals/R_morphism/surjective_map/f.var".
 
-inline procedural "cic:/CoRN/reals/R_morphism/map_is_surjective.con".
+inline procedural "cic:/CoRN/reals/R_morphism/map_is_surjective.con" as definition.
 
 (* UNEXPORTED
 End surjective_map
@@ -212,7 +212,7 @@ alias id "f" = "cic:/CoRN/reals/R_morphism/simplification/f.var".
 
 alias id "H1" = "cic:/CoRN/reals/R_morphism/simplification/H1.var".
 
-inline procedural "cic:/CoRN/reals/R_morphism/f_well_def.con".
+inline procedural "cic:/CoRN/reals/R_morphism/f_well_def.con" as lemma.
 
 (* UNEXPORTED
 Section with_less
@@ -220,13 +220,13 @@ Section with_less
 
 alias id "H2" = "cic:/CoRN/reals/R_morphism/simplification/with_less/H2.var".
 
-inline procedural "cic:/CoRN/reals/R_morphism/less_pres_f.con".
+inline procedural "cic:/CoRN/reals/R_morphism/less_pres_f.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/R_morphism/leEq_pres_f.con".
+inline procedural "cic:/CoRN/reals/R_morphism/leEq_pres_f.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/R_morphism/f_pres_leEq.con".
+inline procedural "cic:/CoRN/reals/R_morphism/f_pres_leEq.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/R_morphism/f_pres_apartness.con".
+inline procedural "cic:/CoRN/reals/R_morphism/f_pres_apartness.con" as lemma.
 
 (* UNEXPORTED
 End with_less
@@ -238,11 +238,11 @@ Section with_plus
 
 alias id "H3" = "cic:/CoRN/reals/R_morphism/simplification/with_plus/H3.var".
 
-inline procedural "cic:/CoRN/reals/R_morphism/f_pres_Zero.con".
+inline procedural "cic:/CoRN/reals/R_morphism/f_pres_Zero.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/R_morphism/f_pres_minus.con".
+inline procedural "cic:/CoRN/reals/R_morphism/f_pres_minus.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/R_morphism/f_pres_min.con".
+inline procedural "cic:/CoRN/reals/R_morphism/f_pres_min.con" as lemma.
 
 (* UNEXPORTED
 End with_plus
@@ -256,7 +256,7 @@ alias id "H2" = "cic:/CoRN/reals/R_morphism/simplification/with_plus_less/H2.var
 
 alias id "H3" = "cic:/CoRN/reals/R_morphism/simplification/with_plus_less/H3.var".
 
-inline procedural "cic:/CoRN/reals/R_morphism/f_pres_ap_zero.con".
+inline procedural "cic:/CoRN/reals/R_morphism/f_pres_ap_zero.con" as lemma.
 
 (* UNEXPORTED
 Section surjectivity_helps
@@ -264,7 +264,7 @@ Section surjectivity_helps
 
 alias id "f_surj" = "cic:/CoRN/reals/R_morphism/simplification/with_plus_less/surjectivity_helps/f_surj.var".
 
-inline procedural "cic:/CoRN/reals/R_morphism/f_pres_Lim.con".
+inline procedural "cic:/CoRN/reals/R_morphism/f_pres_Lim.con" as lemma.
 
 (* UNEXPORTED
 End surjectivity_helps
@@ -276,11 +276,11 @@ Section with_mult_plus_less
 
 alias id "H4" = "cic:/CoRN/reals/R_morphism/simplification/with_plus_less/with_mult_plus_less/H4.var".
 
-inline procedural "cic:/CoRN/reals/R_morphism/f_pres_one.con".
+inline procedural "cic:/CoRN/reals/R_morphism/f_pres_one.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/R_morphism/f_pres_inv.con".
+inline procedural "cic:/CoRN/reals/R_morphism/f_pres_inv.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/R_morphism/simplified_Homomorphism.con".
+inline procedural "cic:/CoRN/reals/R_morphism/simplified_Homomorphism.con" as definition.
 
 (* UNEXPORTED
 End with_mult_plus_less