added atomize_iff;

--- 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