....

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma
index 58c4f9c581718941e5df6ff10135aa0e93e44ff2..3cbb70058ca879290b8f92a8f41d7996fb46e02a 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma
@@ -87,7 +87,7 @@ definition Oid_relation_pair: ∀o:Obasic_pair. Orelation_pair o o.
   | lapply (id_neutral_right2 ? (Oconcr o) ? (⊩)) as H;
     lapply (id_neutral_left2 ?? (Oform o) (⊩)) as H1;
     apply (.= H);
-    apply (H1 \sup -1);]
+    apply (H1^-1);]
 qed.
 
 lemma Orelation_pair_composition:
@@ -121,11 +121,11 @@ intros;
     apply rule (.= ASSOC);
     apply (.= #‡e1);
     apply (.= #‡(Ocommute ?? b'));
-    apply rule (.= ASSOC \sup -1);
+    apply rule (.= ASSOC^-1);
     apply (.= e‡#);
     apply rule (.= ASSOC);
-    apply (.= #‡(Ocommute ?? b')\sup -1);
-    apply rule (ASSOC \sup -1);
+    apply (.= #‡(Ocommute ?? b')^-1);
+    apply rule (ASSOC^-1);
 qed.
 
 definition Orelation_pair_composition_morphism:

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
index f2ce654bae925b1dd036d565c5aecf0a27351112..245fc4fdbf866ee9c9a28d521bb790c5f5cf4489 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
@@ -106,13 +106,13 @@ definition Ocontinuous_relation_comp:
   | intros;
     apply sym1; 
     change in match ((s ∘ r) U) with (s (r U));
-    apply (.= (Oreduced : ?)\sup -1);
+    apply (.= (Oreduced : ?)^-1);
      [ apply (.= (Oreduced :?)); [ assumption | apply refl1 ]
      | apply refl1]
   | intros;
     apply sym1;
     change in match ((s ∘ r)⎻* U) with (s⎻* (r⎻* U));
-    apply (.= (Osaturated : ?)\sup -1);
+    apply (.= (Osaturated : ?)^-1);
      [ apply (.= (Osaturated : ?)); [ assumption | apply refl1 ]
      | apply refl1]]
 qed.