src/HOL/Filter.thy
changeset 62102 877463945ce9
parent 62101 26c0a70f78a3
child 62123 df65f5c27c15
     1.1 --- a/src/HOL/Filter.thy	Fri Jan 08 17:40:59 2016 +0100
     1.2 +++ b/src/HOL/Filter.thy	Fri Jan 08 17:41:04 2016 +0100
     1.3 @@ -26,6 +26,11 @@
     1.4    show "(\<lambda>x. True) \<in> ?filter" by (auto intro: is_filter.intro)
     1.5  qed
     1.6  
     1.7 +text \<open>Kill code generation for filters\<close>
     1.8 +
     1.9 +code_datatype Abs_filter
    1.10 +declare [[code abort: Rep_filter]]
    1.11 +
    1.12  lemma is_filter_Rep_filter: "is_filter (Rep_filter F)"
    1.13    using Rep_filter [of F] by simp
    1.14