--- a/src/HOL/Nominal/Nominal.thy Mon Jun 05 14:26:07 2006 +0200
+++ b/src/HOL/Nominal/Nominal.thy Mon Jun 05 18:38:41 2006 +0200
@@ -985,6 +985,15 @@
section {* further lemmas for permutation types *}
(*==============================================*)
+lemma perm_diff:
+ fixes X::"'a set"
+ and Y::"'a set"
+ and pi::"'x prm"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "pi \<bullet> (X - Y) = (pi \<bullet> X) - (pi \<bullet> Y)"
+ by (auto simp add: perm_set_def pt_bij[OF pt, OF at])
+
lemma pt_rev_pi:
fixes pi :: "'x prm"
and x :: "'a"