- notation (possibly affecting all .ma files):

[helm.git] / matita / matita / library / didactic / exercises / shannon.ma

diff --git a/matita/matita/library/didactic/exercises/shannon.ma b/matita/matita/library/didactic/exercises/shannon.ma
index 78504385ffe20f0e267e0cbc74d6e076c83cf430..c3aa746c8cf84f101b2f3265f8dbc0f0a3b74f79 100644 (file)
--- a/matita/matita/library/didactic/exercises/shannon.ma
+++ b/matita/matita/library/didactic/exercises/shannon.ma
@@ -114,7 +114,7 @@ notation > "t [ term 90 a / term 90 b]" non associative with precedence 19 for @
 interpretation "Substitution for Formula" 'substitution b a t = (subst b a t).
 definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]v = [[ F2 ]]v.
 notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)"  non associative with precedence 45 for @{ 'equivF $a $b }.
-notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
+notation > "a ≡ b" non associative with precedence 55 for @{ equiv $a $b }.
 interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
 lemma min_1_sem: ∀F,v.min 1 [[ F ]]v = [[ F ]]v. intros; cases (sem_bool F v); rewrite > H; reflexivity; qed.
 lemma max_0_sem: ∀F,v.max [[ F ]]v 0 = [[ F ]]v. intros; cases (sem_bool F v); rewrite > H; reflexivity; qed.