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