changeset 43866 | 8a50dc70cbff |
parent 43818 | fcc5d3ffb6f5 |
child 43898 | 935359fd8210 |
--- 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 {} = {{}}"