# HG changeset patch
# User wenzelm
# Date 1138385124 -3600
# Node ID fc35dcc2558bdc3fd49fb8db9881d7d50fe5d368
# Parent  a4554848b59eb24892dd315abe5a7d45f8a86f6a
added atomize_iff;

diff -r a4554848b59e -r fc35dcc2558b src/FOL/IFOL.thy
--- 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