X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flibrary%2Fdidactic%2Fexercises%2Fshannon.ma;fp=matita%2Fmatita%2Flibrary%2Fdidactic%2Fexercises%2Fshannon.ma;h=c3aa746c8cf84f101b2f3265f8dbc0f0a3b74f79;hb=eaaea3c18083de3e442e939768ff450d3b093911;hp=78504385ffe20f0e267e0cbc74d6e076c83cf430;hpb=dc66c8d89a5147178ccdacb8341ed26c9c52f06b;p=helm.git

diff --git a/matita/matita/library/didactic/exercises/shannon.ma b/matita/matita/library/didactic/exercises/shannon.ma
index 78504385f..c3aa746c8 100644
--- 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.