src/HOL/HOL.thy
changeset 57512 cc97b347b301
parent 56941 952833323c99
child 57948 75724d71013c
     1.1 --- a/src/HOL/HOL.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -977,10 +977,10 @@
     1.4    by blast
     1.5  
     1.6  lemma eq_ac:
     1.7 -  shows eq_commute: "(a=b) = (b=a)"
     1.8 -    and eq_left_commute: "(P=(Q=R)) = (Q=(P=R))"
     1.9 -    and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (iprover, blast+)
    1.10 -lemma neq_commute: "(a~=b) = (b~=a)" by iprover
    1.11 +  shows eq_commute: "a = b \<longleftrightarrow> b = a"
    1.12 +    and iff_left_commute: "(P \<longleftrightarrow> (Q \<longleftrightarrow> R)) \<longleftrightarrow> (Q \<longleftrightarrow> (P \<longleftrightarrow> R))"
    1.13 +    and iff_assoc: "((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))" by (iprover, blast+)
    1.14 +lemma neq_commute: "a \<noteq> b \<longleftrightarrow> b \<noteq> a" by iprover
    1.15  
    1.16  lemma conj_comms:
    1.17    shows conj_commute: "(P&Q) = (Q&P)"