--- 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 *}