# HG changeset patch
# User krauss
# Date 1314273994 -7200
# Node ID e3e8d20a6ebcc883e7c478a163babf5c20bc6ede
# Parent  6cddca146ca0f8f2bf4c117b997296cd18e51142
lemma Compl_insert: "- insert x A = (-A) - {x}"

diff -r 6cddca146ca0 -r e3e8d20a6ebc src/HOL/Set.thy
--- 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