# HG changeset patch
# User haftmann
# Date 1264961223 -3600
# Node ID 6676fd863e02727bf4702b43971a78f94f771c99
# Parent  8cb6e7a42e9cceeaa1cb8eee575982907737ef12
adjusted to changes in List_Set.thy

diff -r 8cb6e7a42e9c -r 6676fd863e02 src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Sun Jan 31 14:51:32 2010 +0100
+++ b/src/HOL/Library/Executable_Set.thy	Sun Jan 31 19:07:03 2010 +0100
@@ -93,14 +93,14 @@
   by simp
 
 lemma insert_Set [code]:
-  "insert x (Set xs) = Set (List_Set.insert x xs)"
-  "insert x (Coset xs) = Coset (remove_all x xs)"
-  by (simp_all add: insert_set insert_set_compl)
+  "insert x (Set xs) = Set (List.insert x xs)"
+  "insert x (Coset xs) = Coset (removeAll x xs)"
+  by (simp_all add: set_insert)
 
 lemma remove_Set [code]:
-  "remove x (Set xs) = Set (remove_all x xs)"
-  "remove x (Coset xs) = Coset (List_Set.insert x xs)"
-  by (simp_all add:remove_set remove_set_compl)
+  "remove x (Set xs) = Set (removeAll x xs)"
+  "remove x (Coset xs) = Coset (List.insert x xs)"
+  by (auto simp add: set_insert remove_def)
 
 lemma image_Set [code]:
   "image f (Set xs) = Set (remdups (map f xs))"