--- a/src/HOL/Set.thy Fri Feb 13 09:56:24 2009 +0100
+++ b/src/HOL/Set.thy Fri Feb 13 23:55:04 2009 +0100
@@ -787,6 +787,9 @@
lemma set_diff_eq: "A - B = {x. x : A & ~ x : B}" by blast
+lemma Compl_eq_Diff_UNIV: "-A = (UNIV - A)"
+by blast
+
subsubsection {* Augmenting a set -- insert *}