| changeset 44326 | 2b088d74beb3 |
| parent 42871 | 1c0b99f950d9 |
| child 45012 | 060f76635bfe |
--- a/src/HOL/Library/More_Set.thy Sat Aug 20 01:39:27 2011 +0200 +++ b/src/HOL/Library/More_Set.thy Sat Aug 20 01:40:22 2011 +0200 @@ -50,7 +50,7 @@ lemma remove_set_compl: "remove x (- set xs) = - set (List.insert x xs)" - by (auto simp del: mem_def simp add: remove_def List.insert_def) + by (auto simp add: remove_def List.insert_def) lemma image_set: "image f (set xs) = set (map f xs)"