src/HOL/Isar_Examples/Expr_Compiler.thy
changeset 58310 91ea607a34d8
parent 58260 c96e511bfb79
child 58614 7338eb25226c
     1.1 --- a/src/HOL/Isar_Examples/Expr_Compiler.thy	Thu Sep 11 19:26:59 2014 +0200
     1.2 +++ b/src/HOL/Isar_Examples/Expr_Compiler.thy	Thu Sep 11 19:32:36 2014 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4    consisting of variables, constants, and binary operations on
     1.5    expressions. *}
     1.6  
     1.7 -datatype_new (dead 'adr, dead 'val) expr =
     1.8 +datatype (dead 'adr, dead 'val) expr =
     1.9      Variable 'adr
    1.10    | Constant 'val
    1.11    | Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr"
    1.12 @@ -51,7 +51,7 @@
    1.13  text {* Next we model a simple stack machine, with three
    1.14    instructions. *}
    1.15  
    1.16 -datatype_new (dead 'adr, dead 'val) instr =
    1.17 +datatype (dead 'adr, dead 'val) instr =
    1.18      Const 'val
    1.19    | Load 'adr
    1.20    | Apply "'val binop"