X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Freals%2FBridges_iso.ma;h=99cd76b716c35771e65106b6a4f7f34558da494f;hb=89f42c758bfa3e15324d289774792971f282e684;hp=6c3b241e3550b12ac3f2c225804779978fe2eb00;hpb=5e01cba364607e7937aec2e359c34f049bb0f108;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/reals/Bridges_iso.ma b/helm/software/matita/contribs/CoRN-Decl/reals/Bridges_iso.ma
index 6c3b241e3..99cd76b71 100644
--- a/helm/software/matita/contribs/CoRN-Decl/reals/Bridges_iso.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/reals/Bridges_iso.ma
@@ -44,11 +44,11 @@ inline "cic:/CoRN/reals/Bridges_iso/le_witness_informative.con".
 Section bridges_axioms_imply_ours
 *)
 
-inline "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/OF.var" "bridges_axioms_imply_ours__".
+alias id "OF" = "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/OF.var".
 
-inline "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/lubp.var" "bridges_axioms_imply_ours__".
+alias id "lubp" = "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/lubp.var".
 
-inline "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/is_Archimedes.var" "bridges_axioms_imply_ours__".
+alias id "is_Archimedes" = "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/is_Archimedes.var".
 
 inline "cic:/CoRN/reals/Bridges_iso/is_Archimedes'.con".
 
@@ -64,7 +64,7 @@ inline "cic:/CoRN/reals/Bridges_iso/glbp.con".
 Section supremum
 *)
 
-inline "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/supremum/P.var" "bridges_axioms_imply_ours__proofs_in_TCS__supremum__".
+alias id "P" = "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/supremum/P.var".
 
 inline "cic:/CoRN/reals/Bridges_iso/inequality1.con".
 
@@ -96,7 +96,7 @@ inline "cic:/CoRN/reals/Bridges_iso/kaf.con".
 
 inline "cic:/CoRN/reals/Bridges_iso/Pkaf.con".
 
-inline "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/supremum/is_finite_P.var" "bridges_axioms_imply_ours__proofs_in_TCS__supremum__".
+alias id "is_finite_P" = "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/supremum/is_finite_P.var".
 
 inline "cic:/CoRN/reals/Bridges_iso/card.con".
 
@@ -112,7 +112,7 @@ inline "cic:/CoRN/reals/Bridges_iso/indeks.con".
 
 inline "cic:/CoRN/reals/Bridges_iso/Pindeks.con".
 
-inline "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/supremum/is_onto_seq_P.var" "bridges_axioms_imply_ours__proofs_in_TCS__supremum__".
+alias id "is_onto_seq_P" = "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/supremum/is_onto_seq_P.var".
 
 inline "cic:/CoRN/reals/Bridges_iso/P_is_inhabited.con".
 
@@ -189,7 +189,7 @@ inline "cic:/CoRN/reals/Bridges_iso/bounded_quantifier_informative.con".
 
 inline "cic:/CoRN/reals/Bridges_iso/bridges_lemma1a.con".
 
-inline "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/supremum/P_is_strongly_extensional.var" "bridges_axioms_imply_ours__proofs_in_TCS__supremum__".
+alias id "P_is_strongly_extensional" = "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/supremum/P_is_strongly_extensional.var".
 
 inline "cic:/CoRN/reals/Bridges_iso/bridges_lemma1b.con".
 
@@ -211,7 +211,7 @@ Section Every_Cauchy_Sequence_is_bounded
 
 inline "cic:/CoRN/reals/Bridges_iso/seq2set.con".
 
-inline "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/Every_Cauchy_Sequence_is_bounded/g.var" "bridges_axioms_imply_ours__proofs_in_TCS__Every_Cauchy_Sequence_is_bounded__".
+alias id "g" = "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/Every_Cauchy_Sequence_is_bounded/g.var".
 
 inline "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/Every_Cauchy_Sequence_is_bounded/g_.con" "bridges_axioms_imply_ours__proofs_in_TCS__Every_Cauchy_Sequence_is_bounded__".
 
@@ -263,7 +263,7 @@ inline "cic:/CoRN/reals/Bridges_iso/tail_seq.con".
 End Every_Cauchy_Sequence_is_bounded
 *)
 
-inline "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/g.var" "bridges_axioms_imply_ours__proofs_in_TCS__".
+alias id "g" = "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/g.var".
 
 inline "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/g_.con" "bridges_axioms_imply_ours__proofs_in_TCS__".