--- a/src/HOL/Nominal/Nominal.thy Fri Apr 06 01:26:30 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy Sat Apr 07 11:05:25 2007 +0200
@@ -1090,6 +1090,20 @@
section {* further lemmas for permutation types *}
(*==============================================*)
+lemma swap_simp_a:
+ fixes a ::"'x"
+ and b ::"'x"
+ assumes a: "at TYPE('x)"
+ shows "[(a,b)]\<bullet> a = b"
+ using a by (auto simp add:at_calc)
+
+lemma swap_simp_b:
+ fixes a ::"'x"
+ and b ::"'x"
+ assumes a: "at TYPE('x)"
+ shows "[(a,b)]\<bullet> b = a"
+ using a by (auto simp add:at_calc)
+
lemma pt_rev_pi:
fixes pi :: "'x prm"
and x :: "'a"