src/HOL/Set.thy
changeset 13818 274fda8cca4b
parent 13764 3e180bf68496
child 13826 e94aa103e12d
     1.1 --- a/src/HOL/Set.thy	Fri Feb 14 17:35:56 2003 +0100
     1.2 +++ b/src/HOL/Set.thy	Sun Feb 16 12:16:07 2003 +0100
     1.3 @@ -1251,7 +1251,10 @@
     1.4  lemma Compl_disjoint2 [simp]: "-A \<inter> A = {}"
     1.5    by blast
     1.6  
     1.7 -lemma Compl_partition: "A \<union> (-A) = UNIV"
     1.8 +lemma Compl_partition: "A \<union> -A = UNIV"
     1.9 +  by blast
    1.10 +
    1.11 +lemma Compl_partition2: "-A \<union> A = UNIV"
    1.12    by blast
    1.13  
    1.14  lemma double_complement [simp]: "- (-A) = (A::'a set)"