src/HOL/Set.thy

 lemma Compl_subset_Compl_iff [iff]: "(-A \<subseteq> -B) = (B \<subseteq> A)"
   by (fact compl_le_compl_iff)
 
 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
   (a) they duplicate the body and (b) there are no similar rules for @{text Int}. *}