src/HOL/Set.thy

--- a/src/HOL/Set.thy	Sun Jul 17 15:15:58 2011 +0200
+++ b/src/HOL/Set.thy	Sun Jul 17 19:48:02 2011 +0200
@@ -1487,6 +1487,9 @@
 lemma ex_bool_eq: "(\<exists>b. P b) \<longleftrightarrow> P True \<or> P False"
   by (auto intro: bool_contrapos)
 
+lemma UNIV_bool [no_atp]: "UNIV = {False, True}"
+  by (auto intro: bool_induct)
+
 text {* \medskip @{text Pow} *}
 
 lemma Pow_empty [simp]: "Pow {} = {{}}"