| changeset 46821 | ff6b0c1087f2 |
| parent 46820 | c656222c4dc1 |
| child 58871 | c399ae4b836f |
--- 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