# HG changeset patch
# User paulson
# Date 1028118848 -7200
# Node ID 05631e8f0258ebfd5af3e3933e8b8f557cc74dbf
# Parent  78b93a667c0151d8e785144b247aa7087b4bcd4f
new theorem eq_commute

diff -r 78b93a667c01 -r 05631e8f0258 src/FOL/IFOL.thy
--- 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))"