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)"
```