adding code equation for Collect on finite types
authorbulwahn
Wed Jan 25 09:32:23 2012 +0100 (2012-01-25)
changeset 46329cf3b387ba667
parent 46327 ecda23528833
child 46330 2ddc00f8ad7c
adding code equation for Collect on finite types
src/HOL/Enum.thy
     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