diff -r 4d77568cdb28 -r dbc458262f4c src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Apr 07 21:25:20 2008 +0200
+++ b/src/Pure/Pure.thy	Mon Apr 07 21:25:21 2008 +0200
@@ -20,6 +20,9 @@
 
 lemmas meta_allE = meta_spec [elim_format]
 
+lemma swap_params:
+  "(\<And>x y. PROP P(x, y)) == (\<And>y x. PROP P(x, y))" ..
+
 
 subsection {* Embedded terms *}