src/FOL/IFOL.thy

 next
   assume "x = y"
   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
   assume "!!C. (A ==> B ==> PROP C) ==> PROP C"
   show "A & B" by (rule conjI)