src/HOL/Quickcheck_Narrowing.thy
changeset 58350 919149921e46
parent 58334 7553a1bcecb7
child 58400 d0d3c30806b4
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Tue Sep 16 18:42:33 2014 +0200
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Tue Sep 16 19:23:37 2014 +0200
     1.3 @@ -26,14 +26,14 @@
     1.4  
     1.5  subsubsection {* Narrowing's deep representation of types and terms *}
     1.6  
     1.7 -datatype (plugins only: code) narrowing_type =
     1.8 +datatype (plugins only: code extraction) narrowing_type =
     1.9    Narrowing_sum_of_products "narrowing_type list list"
    1.10  
    1.11 -datatype (plugins only: code) narrowing_term =
    1.12 +datatype (plugins only: code extraction) narrowing_term =
    1.13    Narrowing_variable "integer list" narrowing_type
    1.14  | Narrowing_constructor integer "narrowing_term list"
    1.15  
    1.16 -datatype (plugins only: code) (dead 'a) narrowing_cons =
    1.17 +datatype (plugins only: code extraction) (dead 'a) narrowing_cons =
    1.18    Narrowing_cons narrowing_type "(narrowing_term list \<Rightarrow> 'a) list"
    1.19  
    1.20  primrec map_cons :: "('a => 'b) => 'a narrowing_cons => 'b narrowing_cons"
    1.21 @@ -127,7 +127,7 @@
    1.22  class narrowing =
    1.23    fixes narrowing :: "integer => 'a narrowing_cons"
    1.24  
    1.25 -datatype (plugins only: code) property =
    1.26 +datatype (plugins only: code extraction) property =
    1.27    Universal narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term"
    1.28  | Existential narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term"
    1.29  | Property bool
    1.30 @@ -158,7 +158,7 @@
    1.31  
    1.32  subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *}
    1.33  
    1.34 -datatype (plugins only: code quickcheck_narrowing) (dead 'a, dead 'b) ffun =
    1.35 +datatype (plugins only: code quickcheck_narrowing extraction) (dead 'a, dead 'b) ffun =
    1.36    Constant 'b
    1.37  | Update 'a 'b "('a, 'b) ffun"
    1.38  
    1.39 @@ -170,7 +170,7 @@
    1.40  hide_type (open) ffun
    1.41  hide_const (open) Constant Update eval_ffun
    1.42  
    1.43 -datatype (plugins only: code quickcheck_narrowing) (dead 'b) cfun = Constant 'b
    1.44 +datatype (plugins only: code quickcheck_narrowing extraction) (dead 'b) cfun = Constant 'b
    1.45  
    1.46  primrec eval_cfun :: "'b cfun => 'a => 'b"
    1.47  where