--- a/src/HOL/Library/List_Set.thy Sun Jan 31 14:51:31 2010 +0100
+++ b/src/HOL/Library/List_Set.thy Sun Jan 31 14:51:32 2010 +0100
@@ -7,15 +7,6 @@
imports Main
begin
-subsection {* Various additional list functions *}
-
-definition insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- "insert x xs = (if x \<in> set xs then xs else x # xs)"
-
-definition remove_all :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- "remove_all x xs = filter (Not o op = x) xs"
-
-
subsection {* Various additional set functions *}
definition is_empty :: "'a set \<Rightarrow> bool" where
@@ -61,21 +52,13 @@
"{} = set []"
by simp
-lemma insert_set:
- "Set.insert x (set xs) = set (insert x xs)"
- by (auto simp add: insert_def)
-
lemma insert_set_compl:
- "Set.insert x (- set xs) = - set (List_Set.remove_all x xs)"
- by (auto simp del: mem_def simp add: remove_all_def)
-
-lemma remove_set:
- "remove x (set xs) = set (remove_all x xs)"
- by (auto simp add: remove_def remove_all_def)
+ "insert x (- set xs) = - set (removeAll x xs)"
+ by auto
lemma remove_set_compl:
- "List_Set.remove x (- set xs) = - set (List_Set.insert x xs)"
- by (auto simp del: mem_def simp add: remove_def List_Set.insert_def)
+ "remove x (- set xs) = - set (List.insert x xs)"
+ by (auto simp del: mem_def simp add: remove_def List.insert_def)
lemma image_set:
"image f (set xs) = set (map f xs)"
@@ -128,7 +111,4 @@
"A \<inter> B = project (\<lambda>x. x \<in> A) B"
by (auto simp add: project_def)
-
-hide (open) const insert
-
end
\ No newline at end of file