1.1 --- a/src/HOL/Library/Executable_Set.thy Sun Jan 31 14:51:32 2010 +0100
1.2 +++ b/src/HOL/Library/Executable_Set.thy Sun Jan 31 19:07:03 2010 +0100
1.3 @@ -93,14 +93,14 @@
1.4 by simp
1.5
1.6 lemma insert_Set [code]:
1.7 - "insert x (Set xs) = Set (List_Set.insert x xs)"
1.8 - "insert x (Coset xs) = Coset (remove_all x xs)"
1.9 - by (simp_all add: insert_set insert_set_compl)
1.10 + "insert x (Set xs) = Set (List.insert x xs)"
1.11 + "insert x (Coset xs) = Coset (removeAll x xs)"
1.12 + by (simp_all add: set_insert)
1.13
1.14 lemma remove_Set [code]:
1.15 - "remove x (Set xs) = Set (remove_all x xs)"
1.16 - "remove x (Coset xs) = Coset (List_Set.insert x xs)"
1.17 - by (simp_all add:remove_set remove_set_compl)
1.18 + "remove x (Set xs) = Set (removeAll x xs)"
1.19 + "remove x (Coset xs) = Coset (List.insert x xs)"
1.20 + by (auto simp add: set_insert remove_def)
1.21
1.22 lemma image_Set [code]:
1.23 "image f (Set xs) = Set (remdups (map f xs))"