src/HOL/Enum.thy
changeset 46329 cf3b387ba667
parent 45963 1c7e6454883e
child 46336 39fe503602fb
     1.1 --- a/src/HOL/Enum.thy	Tue Jan 24 09:13:24 2012 +0100
     1.2 +++ b/src/HOL/Enum.thy	Wed Jan 25 09:32:23 2012 +0100
     1.3 @@ -776,11 +776,16 @@
     1.4      unfolding enum_the_def by (auto split: list.split)
     1.5  qed
     1.6  
     1.7 +code_abort enum_the
     1.8 +
     1.9 +subsection {* Further operations on finite types *}
    1.10 +
    1.11 +lemma [code]:
    1.12 +  "Collect P = set (filter P enum)"
    1.13 +by (auto simp add: enum_UNIV)
    1.14  
    1.15  subsection {* Closing up *}
    1.16  
    1.17 -code_abort enum_the
    1.18 -
    1.19  hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
    1.20  
    1.21