X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fbasic_pairs_to_basic_topologies.ma;h=5a98136bc889dc6ef7b5e8ee246580cf9078cab4;hb=e78cf74f8976cf0ca554f64baa9979d0423ee927;hp=576fa5ea157b672268e8f25ac2ae3c9d2df7cca1;hpb=b1dbb34e1e2388a3987710e128e6f19b7d8fe5fc;p=helm.git

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