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