src/HOL/Set.thy
changeset 29901 f4b3f8fbf599
parent 29691 9f03b5f847cd
child 30304 d8e4cd2ac2a1
     1.1 --- a/src/HOL/Set.thy	Fri Feb 13 09:56:24 2009 +0100
     1.2 +++ b/src/HOL/Set.thy	Fri Feb 13 23:55:04 2009 +0100
     1.3 @@ -787,6 +787,9 @@
     1.4  
     1.5  lemma set_diff_eq: "A - B = {x. x : A & ~ x : B}" by blast
     1.6  
     1.7 +lemma Compl_eq_Diff_UNIV: "-A = (UNIV - A)"
     1.8 +by blast
     1.9 +
    1.10  
    1.11  subsubsection {* Augmenting a set -- insert *}
    1.12