lemma Compl_insert: "- insert x A = (-A) - {x}"

--- a/src/HOL/Set.thy	Thu Aug 25 11:15:31 2011 +0200
+++ b/src/HOL/Set.thy	Thu Aug 25 14:06:34 2011 +0200
@@ -1378,6 +1378,9 @@
 lemma Compl_eq_Compl_iff [iff]: "(-A = -B) = (A = (B::'a set))"
   by (fact compl_eq_compl_iff)
 
+lemma Compl_insert: "- insert x A = (-A) - {x}"
+  by blast
+
 text {* \medskip Bounded quantifiers.
 
   The following are not added to the default simpset because