1.1 --- a/src/HOL/Complete_Lattice.thy	Sun Jul 17 15:15:58 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Sun Jul 17 19:48:02 2011 +0200
     1.3 @@ -564,10 +564,6 @@
     1.4    "(\<Sqinter>x\<in>UNIV. f x) = \<Sqinter>range f"
     1.5    by (simp add: INFI_def)
     1.6  
     1.7 -lemma UNIV_bool [no_atp]: -- "FIXME move"
     1.8 -  "UNIV = {False, True}"
     1.9 -  by auto
    1.10 -
    1.11  lemma (in complete_lattice) INF_bool_eq:
    1.12    "(\<Sqinter>b. A b) = A True \<sqinter> A False"
    1.13    by (simp add: UNIV_bool INF_empty INF_insert inf_commute)

     2.1 --- a/src/HOL/Finite_Set.thy	Sun Jul 17 15:15:58 2011 +0200
     2.2 +++ b/src/HOL/Finite_Set.thy	Sun Jul 17 19:48:02 2011 +0200
     2.3 @@ -477,20 +477,14 @@
     2.4  lemma finite [simp]: "finite (A \<Colon> 'a set)"
     2.5    by (rule subset_UNIV finite_UNIV finite_subset)+
     2.6  
     2.7 -lemma finite_code [code]: "finite (A \<Colon> 'a set) = True"
     2.8 +lemma finite_code [code]: "finite (A \<Colon> 'a set) \<longleftrightarrow> True"
     2.9    by simp
    2.10  
    2.11  end
    2.12  
    2.13 -lemma UNIV_unit [no_atp]:
    2.14 -  "UNIV = {()}" by auto
    2.15 -
    2.16  instance unit :: finite proof
    2.17  qed (simp add: UNIV_unit)
    2.18  
    2.19 -lemma UNIV_bool [no_atp]:
    2.20 -  "UNIV = {False, True}" by auto
    2.21 -
    2.22  instance bool :: finite proof
    2.23  qed (simp add: UNIV_bool)
    2.24  

     3.1 --- a/src/HOL/Product_Type.thy	Sun Jul 17 15:15:58 2011 +0200
     3.2 +++ b/src/HOL/Product_Type.thy	Sun Jul 17 19:48:02 2011 +0200
     3.3 @@ -84,9 +84,12 @@
     3.4    f} rather than by @{term [source] "%u. f ()"}.
     3.5  *}
     3.6  
     3.7 -lemma unit_abs_eta_conv [simp,no_atp]: "(%u::unit. f ()) = f"
     3.8 +lemma unit_abs_eta_conv [simp, no_atp]: "(%u::unit. f ()) = f"
     3.9    by (rule ext) simp
    3.10  
    3.11 +lemma UNIV_unit [no_atp]:
    3.12 +  "UNIV = {()}" by auto
    3.13 +
    3.14  instantiation unit :: default
    3.15  begin
    3.16  

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