- transcript: patched to generate aliases instead of inlined variables

[helm.git] / helm / software / matita / contribs / CoRN-Decl / reals / R_morphism.ma

diff --git a/helm/software/matita/contribs/CoRN-Decl/reals/R_morphism.ma b/helm/software/matita/contribs/CoRN-Decl/reals/R_morphism.ma
index 102c89076d64f75bfc76a3c954c2cac210a9b449..5ce1b103c7284126a298148f76bfe0fe31dd8c42 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/reals/R_morphism.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/reals/R_morphism.ma
@@ -16,7 +16,7 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/reals/R_morphism".
 
-include "CoRN_notation.ma".
+include "CoRN.ma".
 
 (* begin hide *)
 
@@ -31,30 +31,30 @@ include "reals/CReals.ma".
 inline "cic:/CoRN/reals/R_morphism/Cauchy_Lim_prop2.con".
 
 (* UNEXPORTED
-Section morphism.
+Section morphism
 *)
 
-inline "cic:/CoRN/reals/R_morphism/R1.var".
+alias id "R1" = "cic:/CoRN/reals/R_morphism/morphism/R1.var".
 
-inline "cic:/CoRN/reals/R_morphism/R2.var".
+alias id "R2" = "cic:/CoRN/reals/R_morphism/morphism/R2.var".
 
 (* UNEXPORTED
-Section morphism_details.
+Section morphism_details
 *)
 
-inline "cic:/CoRN/reals/R_morphism/phi.var".
+alias id "phi" = "cic:/CoRN/reals/R_morphism/morphism/morphism_details/phi.var".
 
-inline "cic:/CoRN/reals/R_morphism/p1.var".
+alias id "p1" = "cic:/CoRN/reals/R_morphism/morphism/morphism_details/p1.var".
 
-inline "cic:/CoRN/reals/R_morphism/p2.var".
+alias id "p2" = "cic:/CoRN/reals/R_morphism/morphism/morphism_details/p2.var".
 
-inline "cic:/CoRN/reals/R_morphism/f1.var".
+alias id "f1" = "cic:/CoRN/reals/R_morphism/morphism/morphism_details/f1.var".
 
-inline "cic:/CoRN/reals/R_morphism/f2.var".
+alias id "f2" = "cic:/CoRN/reals/R_morphism/morphism/morphism_details/f2.var".
 
-inline "cic:/CoRN/reals/R_morphism/g1.var".
+alias id "g1" = "cic:/CoRN/reals/R_morphism/morphism/morphism_details/g1.var".
 
-inline "cic:/CoRN/reals/R_morphism/g2.var".
+alias id "g2" = "cic:/CoRN/reals/R_morphism/morphism/morphism_details/g2.var".
 
 inline "cic:/CoRN/reals/R_morphism/fun_pres_relation.con".
 
@@ -70,12 +70,12 @@ Definition fun_pres_partial_fun:=(x:R1;H1:x[#]Zero;H2:(phi x)[#]Zero)
 inline "cic:/CoRN/reals/R_morphism/fun_pres_Lim.con".
 
 (* UNEXPORTED
-End morphism_details.
+End morphism_details
 *)
 
 inline "cic:/CoRN/reals/R_morphism/Homomorphism.ind".
 
-coercion "cic:/matita/CoRN-Decl/reals/R_morphism/map.con" 0 (* compounds *).
+coercion cic:/matita/CoRN-Decl/reals/R_morphism/map.con 0 (* compounds *).
 
 (* This might be useful later... 
 Definition Homo_as_CSetoid_fun:=
@@ -121,22 +121,22 @@ inline "cic:/CoRN/reals/R_morphism/map_pres_one_unfolded.con".
 inline "cic:/CoRN/reals/R_morphism/map_pres_inv_unfolded.con".
 
 (* UNEXPORTED
-End morphism.
+End morphism
 *)
 
 (* UNEXPORTED
-Section composition.
+Section composition
 *)
 
-inline "cic:/CoRN/reals/R_morphism/R1.var".
+alias id "R1" = "cic:/CoRN/reals/R_morphism/composition/R1.var".
 
-inline "cic:/CoRN/reals/R_morphism/R2.var".
+alias id "R2" = "cic:/CoRN/reals/R_morphism/composition/R2.var".
 
-inline "cic:/CoRN/reals/R_morphism/R3.var".
+alias id "R3" = "cic:/CoRN/reals/R_morphism/composition/R3.var".
 
-inline "cic:/CoRN/reals/R_morphism/f.var".
+alias id "f" = "cic:/CoRN/reals/R_morphism/composition/f.var".
 
-inline "cic:/CoRN/reals/R_morphism/g.var".
+alias id "g" = "cic:/CoRN/reals/R_morphism/composition/g.var".
 
 inline "cic:/CoRN/reals/R_morphism/compose.con".
 
@@ -153,72 +153,72 @@ inline "cic:/CoRN/reals/R_morphism/compose_pres_Lim.con".
 inline "cic:/CoRN/reals/R_morphism/Compose.con".
 
 (* UNEXPORTED
-End composition.
+End composition
 *)
 
 (* UNEXPORTED
-Section isomorphism.
+Section isomorphism
 *)
 
-inline "cic:/CoRN/reals/R_morphism/R1.var".
+alias id "R1" = "cic:/CoRN/reals/R_morphism/isomorphism/R1.var".
 
-inline "cic:/CoRN/reals/R_morphism/R2.var".
+alias id "R2" = "cic:/CoRN/reals/R_morphism/isomorphism/R2.var".
 
 (* UNEXPORTED
-Section identity_map.
+Section identity_map
 *)
 
-inline "cic:/CoRN/reals/R_morphism/R3.var".
+alias id "R3" = "cic:/CoRN/reals/R_morphism/isomorphism/identity_map/R3.var".
 
-inline "cic:/CoRN/reals/R_morphism/f.var".
+alias id "f" = "cic:/CoRN/reals/R_morphism/isomorphism/identity_map/f.var".
 
 inline "cic:/CoRN/reals/R_morphism/map_is_id.con".
 
 (* UNEXPORTED
-End identity_map.
+End identity_map
 *)
 
 inline "cic:/CoRN/reals/R_morphism/Isomorphism.ind".
 
 (* UNEXPORTED
-End isomorphism.
+End isomorphism
 *)
 
 (* UNEXPORTED
-Section surjective_map.
+Section surjective_map
 *)
 
-inline "cic:/CoRN/reals/R_morphism/R1.var".
+alias id "R1" = "cic:/CoRN/reals/R_morphism/surjective_map/R1.var".
 
-inline "cic:/CoRN/reals/R_morphism/R2.var".
+alias id "R2" = "cic:/CoRN/reals/R_morphism/surjective_map/R2.var".
 
-inline "cic:/CoRN/reals/R_morphism/f.var".
+alias id "f" = "cic:/CoRN/reals/R_morphism/surjective_map/f.var".
 
 inline "cic:/CoRN/reals/R_morphism/map_is_surjective.con".
 
 (* UNEXPORTED
-End surjective_map.
+End surjective_map
 *)
 
 (* UNEXPORTED
-Section simplification.
+Section simplification
 *)
 
-inline "cic:/CoRN/reals/R_morphism/R1.var".
+alias id "R1" = "cic:/CoRN/reals/R_morphism/simplification/R1.var".
 
-inline "cic:/CoRN/reals/R_morphism/R2.var".
+alias id "R2" = "cic:/CoRN/reals/R_morphism/simplification/R2.var".
 
-inline "cic:/CoRN/reals/R_morphism/f.var".
+alias id "f" = "cic:/CoRN/reals/R_morphism/simplification/f.var".
 
-inline "cic:/CoRN/reals/R_morphism/H1.var".
+alias id "H1" = "cic:/CoRN/reals/R_morphism/simplification/H1.var".
 
 inline "cic:/CoRN/reals/R_morphism/f_well_def.con".
 
 (* UNEXPORTED
-Section with_less.
+Section with_less
 *)
 
-inline "cic:/CoRN/reals/R_morphism/H2.var".
+alias id "H2" = "cic:/CoRN/reals/R_morphism/simplification/with_less/H2.var".
 
 inline "cic:/CoRN/reals/R_morphism/less_pres_f.con".
 
@@ -229,14 +229,14 @@ inline "cic:/CoRN/reals/R_morphism/f_pres_leEq.con".
 inline "cic:/CoRN/reals/R_morphism/f_pres_apartness.con".
 
 (* UNEXPORTED
-End with_less.
+End with_less
 *)
 
 (* UNEXPORTED
-Section with_plus.
+Section with_plus
 *)
 
-inline "cic:/CoRN/reals/R_morphism/H3.var".
+alias id "H3" = "cic:/CoRN/reals/R_morphism/simplification/with_plus/H3.var".
 
 inline "cic:/CoRN/reals/R_morphism/f_pres_Zero.con".
 
@@ -245,36 +245,36 @@ inline "cic:/CoRN/reals/R_morphism/f_pres_minus.con".
 inline "cic:/CoRN/reals/R_morphism/f_pres_min.con".
 
 (* UNEXPORTED
-End with_plus.
+End with_plus
 *)
 
 (* UNEXPORTED
-Section with_plus_less.
+Section with_plus_less
 *)
 
-inline "cic:/CoRN/reals/R_morphism/H2.var".
+alias id "H2" = "cic:/CoRN/reals/R_morphism/simplification/with_plus_less/H2.var".
 
-inline "cic:/CoRN/reals/R_morphism/H3.var".
+alias id "H3" = "cic:/CoRN/reals/R_morphism/simplification/with_plus_less/H3.var".
 
 inline "cic:/CoRN/reals/R_morphism/f_pres_ap_zero.con".
 
 (* UNEXPORTED
-Section surjectivity_helps.
+Section surjectivity_helps
 *)
 
-inline "cic:/CoRN/reals/R_morphism/f_surj.var".
+alias id "f_surj" = "cic:/CoRN/reals/R_morphism/simplification/with_plus_less/surjectivity_helps/f_surj.var".
 
 inline "cic:/CoRN/reals/R_morphism/f_pres_Lim.con".
 
 (* UNEXPORTED
-End surjectivity_helps.
+End surjectivity_helps
 *)
 
 (* UNEXPORTED
-Section with_mult_plus_less.
+Section with_mult_plus_less
 *)
 
-inline "cic:/CoRN/reals/R_morphism/H4.var".
+alias id "H4" = "cic:/CoRN/reals/R_morphism/simplification/with_plus_less/with_mult_plus_less/H4.var".
 
 inline "cic:/CoRN/reals/R_morphism/f_pres_one.con".
 
@@ -283,15 +283,15 @@ inline "cic:/CoRN/reals/R_morphism/f_pres_inv.con".
 inline "cic:/CoRN/reals/R_morphism/simplified_Homomorphism.con".
 
 (* UNEXPORTED
-End with_mult_plus_less.
+End with_mult_plus_less
 *)
 
 (* UNEXPORTED
-End with_plus_less.
+End with_plus_less
 *)
 
 (* UNEXPORTED
-End simplification.
+End simplification
 *)
 
 (* end hide *)