diff -r d56e0b30ce5a -r 1535aa1c943a src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Mon May 24 13:48:56 2010 +0200
+++ b/src/HOL/Library/Mapping.thy	Mon May 24 13:48:57 2010 +0200
@@ -6,30 +6,6 @@
 imports Main
 begin
 
-lemma remove1_idem: (*FIXME move to List.thy*)
-  assumes "x \<notin> set xs"
-  shows "remove1 x xs = xs"
-  using assms by (induct xs) simp_all
-
-lemma remove1_insort [simp]:
-  "remove1 x (insort x xs) = xs"
-  by (induct xs) simp_all
-
-lemma sorted_list_of_set_remove:
-  assumes "finite A"
-  shows "sorted_list_of_set (A - {x}) = remove1 x (sorted_list_of_set A)"
-proof (cases "x \<in> A")
-  case False with assms have "x \<notin> set (sorted_list_of_set A)" by simp
-  with False show ?thesis by (simp add: remove1_idem)
-next
-  case True then obtain B where A: "A = insert x B" by (rule Set.set_insert)
-  with assms show ?thesis by simp
-qed
-
-lemma sorted_list_of_set_range [simp]:
-  "sorted_list_of_set {m..<n} = [m..<n]"
-  by (rule sorted_distinct_set_unique) simp_all
-
 subsection {* Type definition and primitive operations *}
 
 datatype ('a, 'b) mapping = Mapping "'a \<rightharpoonup> 'b"