added swap_params;
authorwenzelm
Mon, 07 Apr 2008 21:25:21 +0200
changeset 26570 dbc458262f4c
parent 26569 4d77568cdb28
child 26571 114da911bc41
added swap_params;
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 *}