new theorem eq_commute
authorpaulson
Wed Jul 31 14:34:08 2002 +0200 (2002-07-31)
changeset 1343505631e8f0258
parent 13434 78b93a667c01
child 13436 8fd1d803a3d3
new theorem eq_commute
src/FOL/IFOL.thy
     1.1 --- a/src/FOL/IFOL.thy	Tue Jul 30 11:39:57 2002 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Wed Jul 31 14:34:08 2002 +0200
     1.3 @@ -171,6 +171,12 @@
     1.4    and [Pure.elim?] = iffD1 iffD2 impE
     1.5  
     1.6  
     1.7 +lemma eq_commute: "a=b <-> b=a"
     1.8 +apply (rule iffI) 
     1.9 +apply (erule sym)+
    1.10 +done
    1.11 +
    1.12 +
    1.13  subsection {* Atomizing meta-level rules *}
    1.14  
    1.15  lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"