tuned proof
authorhaftmann
Sat Aug 20 01:40:22 2011 +0200 (2011-08-20)
changeset 443262b088d74beb3
parent 44325 84696670feb1
child 44327 46d5e7f52ba5
tuned proof
src/HOL/Library/More_Set.thy
     1.1 --- a/src/HOL/Library/More_Set.thy	Sat Aug 20 01:39:27 2011 +0200
     1.2 +++ b/src/HOL/Library/More_Set.thy	Sat Aug 20 01:40:22 2011 +0200
     1.3 @@ -50,7 +50,7 @@
     1.4  
     1.5  lemma remove_set_compl:
     1.6    "remove x (- set xs) = - set (List.insert x xs)"
     1.7 -  by (auto simp del: mem_def simp add: remove_def List.insert_def)
     1.8 +  by (auto simp add: remove_def List.insert_def)
     1.9  
    1.10  lemma image_set:
    1.11    "image f (set xs) = set (map f xs)"