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