src/HOL/Finite_Set.thy
changeset 43866 8a50dc70cbff
parent 42875 d1aad0957eb2
child 43991 f4a7697011c5
--- a/src/HOL/Finite_Set.thy	Sun Jul 17 15:15:58 2011 +0200
+++ b/src/HOL/Finite_Set.thy	Sun Jul 17 19:48:02 2011 +0200
@@ -477,20 +477,14 @@
 lemma finite [simp]: "finite (A \<Colon> 'a set)"
   by (rule subset_UNIV finite_UNIV finite_subset)+
 
-lemma finite_code [code]: "finite (A \<Colon> 'a set) = True"
+lemma finite_code [code]: "finite (A \<Colon> 'a set) \<longleftrightarrow> True"
   by simp
 
 end
 
-lemma UNIV_unit [no_atp]:
-  "UNIV = {()}" by auto
-
 instance unit :: finite proof
 qed (simp add: UNIV_unit)
 
-lemma UNIV_bool [no_atp]:
-  "UNIV = {False, True}" by auto
-
 instance bool :: finite proof
 qed (simp add: UNIV_bool)