author | paulson |
Wed, 31 Jul 2002 14:34:08 +0200 | |
changeset 13435 | 05631e8f0258 |
parent 13434 | 78b93a667c01 |
child 13436 | 8fd1d803a3d3 |
src/FOL/IFOL.thy | file | annotate | diff | comparison | revisions |
--- 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))"