# HG changeset patch
# User haftmann
# Date 1313797222 -7200
# Node ID 2b088d74beb3dc949a87e1413cc4fb302f086b89
# Parent  84696670feb1a19ae680f83244032b873e7def7d
tuned proof

diff -r 84696670feb1 -r 2b088d74beb3 src/HOL/Library/More_Set.thy
--- 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)"