diff -r 8daf6ff5e11a -r 40db835442a0 Nominal-General/Nominal2_Atoms.thy
--- a/Nominal-General/Nominal2_Atoms.thy	Wed Apr 28 08:22:20 2010 +0200
+++ b/Nominal-General/Nominal2_Atoms.thy	Wed Apr 28 08:24:46 2010 +0200
@@ -9,44 +9,8 @@
 uses ("nominal_atoms.ML")
 begin
 
-section {* Concrete atom types *}
-
-text {*
-  Class @{text at_base} allows types containing multiple sorts of atoms.
-  Class @{text at} only allows types with a single sort.
-*}
-
-lemma atom_image_cong:
-  shows "(atom ` X = atom ` Y) = (X = Y)"
-  apply(rule inj_image_eq_iff)
-  apply(simp add: inj_on_def)
-  done
+section {* Infrastructure for concrete atom types *}
 
-lemma atom_image_supp:
-  "supp S = supp (atom ` S)"
-  apply(simp add: supp_def)
-  apply(simp add: image_eqvt)
-  apply(subst (2) permute_fun_def)
-  apply(simp add: atom_eqvt)
-  apply(simp add: atom_image_cong)
-  done
-
-lemma supp_finite_at_set:
-  assumes a: "finite S"
-  shows "supp S = atom ` S"
-proof -
-  have fin: "finite (atom ` S)" 
-    using a by (simp add: finite_imageI) 
-  have "supp S = supp (atom ` S)" by (rule atom_image_supp)
-  also have "\<dots> = atom ` S" using fin by (simp add: supp_finite_atom_set)
-  finally show "supp S = atom ` S" by simp
-qed
-
-lemma supp_at_insert:
-  fixes a::"'a::at_base"
-  assumes a: "finite S"
-  shows "supp (insert a S) = supp a \<union> supp S"
-  using a by (simp add: supp_finite_at_set supp_at_base)
 
 section {* A swapping operation for concrete atoms *}