From df018fb5614e932492d30f7388883d532b70709a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 1 Feb 2009 18:17:40 +0000 Subject: [PATCH] Renaming. --- .../overlap/basic_pairs_to_basic_topologies.ma | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_basic_topologies.ma index 576fa5ea1..5a98136bc 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_basic_topologies.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_basic_topologies.ma @@ -23,11 +23,11 @@ definition basic_topology_of_basic_pair: basic_pair → basic_topology. letin obt ≝ (o_basic_topology_of_o_basic_pair obp); constructor 1; [ apply (form bp); - | apply (A obt); - | apply (J obt); - | apply (A_is_saturation obt); - | apply (J_is_reduction obt); - | apply (compatibility obt); ] + | apply (oA obt); + | apply (oJ obt); + | apply (oA_is_saturation obt); + | apply (oJ_is_reduction obt); + | apply (Ocompatibility obt); ] qed. definition continuous_relation_of_relation_pair: @@ -38,6 +38,6 @@ definition continuous_relation_of_relation_pair: letin ocr ≝ (o_continuous_relation_of_o_relation_pair ?? orp); constructor 1; [ apply (rp \sub \f); - | apply (reduced ?? ocr); - | apply (saturated ?? ocr); ] + | apply (Oreduced ?? ocr); + | apply (Osaturated ?? ocr); ] qed. \ No newline at end of file -- 2.39.2