From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 18 Jun 2010 11:11:43 +0000 (+0000)
Subject: ....
X-Git-Tag: make_still_working~2894
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c2123cdb49560cc6ef2a86b71ab21b432581c076;p=helm.git

....
---

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 58c4f9c58..3cbb70058 100644
--- 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 f2ce654ba..245fc4fdb 100644
--- 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.