src/HOL/Quickcheck_Narrowing.thy
changeset 58310 91ea607a34d8
parent 58152 6fe60a9a5bad
child 58334 7553a1bcecb7
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Thu Sep 11 19:26:59 2014 +0200
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Sep 11 19:32:36 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_new narrowing_type =
     1.8 +datatype narrowing_type =
     1.9    Narrowing_sum_of_products "narrowing_type list list"
    1.10  
    1.11 -datatype_new narrowing_term =
    1.12 +datatype narrowing_term =
    1.13    Narrowing_variable "integer list" narrowing_type
    1.14  | Narrowing_constructor integer "narrowing_term list"
    1.15  
    1.16 -datatype_new (dead 'a) narrowing_cons =
    1.17 +datatype (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_new property = Universal narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Existential narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Property bool
    1.26 +datatype property = Universal narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Existential narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Property bool
    1.27  
    1.28  (* FIXME: hard-wired maximal depth of 100 here *)
    1.29  definition exists :: "('a :: {narrowing, partial_term_of} => property) => property"
    1.30 @@ -155,7 +155,7 @@
    1.31  
    1.32  subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *}
    1.33  
    1.34 -datatype_new (dead 'a, dead 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun"
    1.35 +datatype (dead 'a, dead 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun"
    1.36  
    1.37  primrec eval_ffun :: "('a, 'b) ffun => 'a => 'b"
    1.38  where
    1.39 @@ -165,7 +165,7 @@
    1.40  hide_type (open) ffun
    1.41  hide_const (open) Constant Update eval_ffun
    1.42  
    1.43 -datatype_new (dead 'b) cfun = Constant 'b
    1.44 +datatype (dead 'b) cfun = Constant 'b
    1.45  
    1.46  primrec eval_cfun :: "'b cfun => 'a => 'b"
    1.47  where