# HG changeset patch
# User paulson
# Date 1045394167 -3600
# Node ID 274fda8cca4b5c008c5da495e6c1770b169abb93
# Parent  7e031a968443e5f115c3bd4c4f0ed13fbdc040aa
new theorem Compl_partition2

diff -r 7e031a968443 -r 274fda8cca4b src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Feb 14 17:35:56 2003 +0100
+++ b/src/HOL/Set.thy	Sun Feb 16 12:16:07 2003 +0100
@@ -1251,7 +1251,10 @@
 lemma Compl_disjoint2 [simp]: "-A \<inter> A = {}"
   by blast
 
-lemma Compl_partition: "A \<union> (-A) = UNIV"
+lemma Compl_partition: "A \<union> -A = UNIV"
+  by blast
+
+lemma Compl_partition2: "-A \<union> A = UNIV"
   by blast
 
 lemma double_complement [simp]: "- (-A) = (A::'a set)"