--- a/src/HOL/Nominal/Nominal.thy Sat Apr 07 11:05:25 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy Sat Apr 07 11:36:35 2007 +0200
@@ -443,6 +443,14 @@
(* rules to calculate simple premutations *)
lemmas at_calc = at2 at1 at3
+lemma at_swap_simps:
+ fixes a ::"'x"
+ and b ::"'x"
+ assumes a: "at TYPE('x)"
+ shows "[(a,b)]\<bullet>a = b"
+ and "[(a,b)]\<bullet>b = a"
+ using a by (simp_all add: at_calc)
+
lemma at4:
assumes a: "at TYPE('x)"
shows "infinite (UNIV::'x set)"
@@ -1090,20 +1098,6 @@
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"