--- a/Nominal/Nominal2_FSet.thy	Sun Nov 14 11:05:22 2010 +0000
+++ b/Nominal/Nominal2_FSet.thy	Sun Nov 14 11:46:39 2010 +0000
@@ -4,43 +4,6 @@
 begin
 
 
-lemma atom_map_fset_cong:
-  shows "map_fset atom x = map_fset atom y \<longleftrightarrow> x = y"
-  apply(rule inj_map_fset_cong)
-  apply(simp add: inj_on_def)
-  done
 
-lemma supp_map_fset_atom:
-  shows "supp (map_fset atom S) = supp S"
-  unfolding supp_def
-  apply(perm_simp)
-  apply(simp add: atom_map_fset_cong)
-  done
-
-lemma supp_at_fset:
-  fixes S::"('a::at_base) fset"
-  shows "supp S = fset (map_fset atom S)"
-  apply (induct S)
-  apply (simp add: supp_empty_fset)
-  apply (simp add: supp_insert_fset)
-  apply (simp add: supp_at_base)
-  done
-
-lemma fresh_star_atom:
-  fixes a::"'a::at_base"
-  shows "fset S \<sharp>* a \<Longrightarrow> atom a \<sharp> fset S"
-  apply (induct S)
-  apply (simp add: fresh_set_empty)
-  apply simp
-  apply (unfold fresh_def)
-  apply (simp add: supp_of_finite_insert)
-  apply (rule conjI)
-  apply (unfold fresh_star_def)
-  apply simp
-  apply (unfold fresh_def)
-  apply (simp add: supp_at_base supp_atom)
-  apply clarify
-  apply auto
-  done
 
 end