more notation

[helm.git] / helm / software / matita / library / formal_topology / o-algebra.ma

diff --git a/helm/software/matita/library/formal_topology/o-algebra.ma b/helm/software/matita/library/formal_topology/o-algebra.ma
index ed363cd2d6045a41ab4e90a35a6a03c4ae09637e..67ff5140e1f12fddc135b00a193b5a817913086c 100644 (file)
--- a/helm/software/matita/library/formal_topology/o-algebra.ma
+++ b/helm/software/matita/library/formal_topology/o-algebra.ma
@@ -80,7 +80,7 @@ record OAlgebra : Type2 := {
   oa_zero_bot: ∀p:oa_P.𝟘 ≤ p;
   oa_one_top: ∀p:oa_P.p ≤ 𝟙;
   oa_overlap_preserves_meet_: ∀p,q:oa_P.p >< q → 
-        p >< (⋀ { x ∈ BOOL | If x then p else q(*match x with [ true ⇒ p | false ⇒ q ]*) | IF_THEN_ELSE_p oa_P p q });
+        p >< (⋀ { x ∈ BOOL | If x then p else q | IF_THEN_ELSE_p oa_P p q });
   oa_join_split: ∀I:SET.∀p.∀q:I ⇒_2 oa_P.p >< (⋁ q) = (∃i:I.p >< (q i));
   (*oa_base : setoid;
   1) enum non e' il nome giusto perche' non e' suriettiva