src/FOL/IFOL.thy
changeset 18813 fc35dcc2558b
parent 18708 4b3dadb4fe33
child 18861 38269ef5175a
--- a/src/FOL/IFOL.thy	Fri Jan 27 19:03:19 2006 +0100
+++ b/src/FOL/IFOL.thy	Fri Jan 27 19:05:24 2006 +0100
@@ -239,6 +239,15 @@
   thus "x == y" by (rule eq_reflection)
 qed
 
+lemma atomize_iff [atomize]: "(A == B) == Trueprop (A <-> B)"
+proof
+  assume "A == B"
+  show "A <-> B" by (unfold prems) (rule iff_refl)
+next
+  assume "A <-> B"
+  thus "A == B" by (rule iff_reflection)
+qed
+
 lemma atomize_conj [atomize]:
   "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
 proof