1.1 --- a/src/HOL/Finite_Set.thy	Sun Jul 17 15:15:58 2011 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Sun Jul 17 19:48:02 2011 +0200
     1.3 @@ -477,20 +477,14 @@
     1.4  lemma finite [simp]: "finite (A \<Colon> 'a set)"
     1.5    by (rule subset_UNIV finite_UNIV finite_subset)+
     1.6  
     1.7 -lemma finite_code [code]: "finite (A \<Colon> 'a set) = True"
     1.8 +lemma finite_code [code]: "finite (A \<Colon> 'a set) \<longleftrightarrow> True"
     1.9    by simp
    1.10  
    1.11  end
    1.12  
    1.13 -lemma UNIV_unit [no_atp]:
    1.14 -  "UNIV = {()}" by auto
    1.15 -
    1.16  instance unit :: finite proof
    1.17  qed (simp add: UNIV_unit)
    1.18  
    1.19 -lemma UNIV_bool [no_atp]:
    1.20 -  "UNIV = {False, True}" by auto
    1.21 -
    1.22  instance bool :: finite proof
    1.23  qed (simp add: UNIV_bool)
    1.24