changeset 13435 | 05631e8f0258 |
parent 12937 | 0c4fd7529467 |
child 13779 | 2a34dc5cf79e |
--- a/src/FOL/IFOL.thy Tue Jul 30 11:39:57 2002 +0200 +++ b/src/FOL/IFOL.thy Wed Jul 31 14:34:08 2002 +0200 @@ -171,6 +171,12 @@ and [Pure.elim?] = iffD1 iffD2 impE +lemma eq_commute: "a=b <-> b=a" +apply (rule iffI) +apply (erule sym)+ +done + + subsection {* Atomizing meta-level rules *} lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"