src/HOL/Set.thy
changeset 43866 8a50dc70cbff
parent 43818 fcc5d3ffb6f5
child 43898 935359fd8210
     1.1 --- a/src/HOL/Set.thy	Sun Jul 17 15:15:58 2011 +0200
     1.2 +++ b/src/HOL/Set.thy	Sun Jul 17 19:48:02 2011 +0200
     1.3 @@ -1487,6 +1487,9 @@
     1.4  lemma ex_bool_eq: "(\<exists>b. P b) \<longleftrightarrow> P True \<or> P False"
     1.5    by (auto intro: bool_contrapos)
     1.6  
     1.7 +lemma UNIV_bool [no_atp]: "UNIV = {False, True}"
     1.8 +  by (auto intro: bool_induct)
     1.9 +
    1.10  text {* \medskip @{text Pow} *}
    1.11  
    1.12  lemma Pow_empty [simp]: "Pow {} = {{}}"