# HG changeset patch
# User haftmann
# Date 1305872173 -7200
# Node ID 1608daf27c1f189f532f7f95f698a170b3e2b63d
# Parent  760094e49a2c0c37921ba71a5e070a6c9be3e1cc
tuned proof

diff -r 760094e49a2c -r 1608daf27c1f src/HOL/Library/More_Set.thy
--- a/src/HOL/Library/More_Set.thy	Tue May 17 15:00:39 2011 +0200
+++ b/src/HOL/Library/More_Set.thy	Fri May 20 08:16:13 2011 +0200
@@ -124,6 +124,6 @@
 
 lemma not_set_compl:
   "Not \<circ> set xs = - set xs"
-  by (simp add: fun_Compl_def bool_Compl_def comp_def fun_eq_iff)
+  by (simp add: fun_Compl_def comp_def fun_eq_iff)
 
 end