diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/Bool.thy
--- a/src/ZF/Bool.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Bool.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -164,10 +164,10 @@
 lemma [simp,TC]: "bool_of_o(P) \<in> bool"
 by (simp add: bool_of_o_def)
 
-lemma [simp]: "(bool_of_o(P) = 1) <-> P"
+lemma [simp]: "(bool_of_o(P) = 1) \<longleftrightarrow> P"
 by (simp add: bool_of_o_def)
 
-lemma [simp]: "(bool_of_o(P) = 0) <-> ~P"
+lemma [simp]: "(bool_of_o(P) = 0) \<longleftrightarrow> ~P"
 by (simp add: bool_of_o_def)
 
 end