Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
new theorem Compl_partition2
authorpaulson
Sun, 16 Feb 2003 12:16:07 +0100
changeset 13818 274fda8cca4b
parent 13817 7e031a968443
child 13819 78f5885b76a9
new theorem Compl_partition2
src/HOL/Set.thy file | annotate | diff | comparison | revisions 
--- 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)"
isabelle