diff -r 95e6eb9044fe -r f4b3f8fbf599 src/HOL/Set.thy
--- 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 *}