--- a/Nominal/Nominal2_Eqvt.thy	Mon Nov 29 05:17:41 2010 +0000
+++ b/Nominal/Nominal2_Eqvt.thy	Mon Nov 29 08:01:09 2010 +0000
@@ -155,15 +155,6 @@
   unfolding Ball_def
   by (perm_simp) (rule refl)
 
-lemma supp_set_empty:
-  shows "supp {} = {}"
-  unfolding supp_def
-  by (simp add: empty_eqvt)
-
-lemma fresh_set_empty:
-  shows "a \<sharp> {}"
-  by (simp add: fresh_def supp_set_empty)
-
 lemma UNIV_eqvt[eqvt]:
   shows "p \<bullet> UNIV = UNIV"
   unfolding UNIV_def
@@ -216,14 +207,6 @@
   shows "p \<bullet> finite A = finite (p \<bullet> A)"
   unfolding finite_permute_iff permute_bool_def ..
 
-lemma supp_set:
-  fixes xs :: "('a::fs) list"
-  shows "supp (set xs) = supp xs"
-apply(induct xs)
-apply(simp add: supp_set_empty supp_Nil)
-apply(simp add: supp_Cons supp_of_finite_insert)
-done
-
 
 section {* List Operations *}
 
@@ -231,14 +214,6 @@
   shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)"
   by (induct xs) auto
 
-lemma supp_append:
-  shows "supp (xs @ ys) = supp xs \<union> supp ys"
-  by (induct xs) (auto simp add: supp_Nil supp_Cons)
-
-lemma fresh_append:
-  shows "a \<sharp> (xs @ ys) \<longleftrightarrow> a \<sharp> xs \<and> a \<sharp> ys"
-  by (induct xs) (simp_all add: fresh_Nil fresh_Cons)
-
 lemma rev_eqvt[eqvt]:
   shows "p \<bullet> (rev xs) = rev (p \<bullet> xs)"
   by (induct xs) (simp_all add: append_eqvt)