src/HOL/Isar_Examples/Expr_Compiler.thy
changeset 35416 d8d7d1b785af
parent 33026 8f35633c4922
child 37671 fa53d267dab3
     1.1 --- a/src/HOL/Isar_Examples/Expr_Compiler.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Isar_Examples/Expr_Compiler.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -85,8 +85,7 @@
     1.4      | Apply f => exec instrs (f (hd stack) (hd (tl stack))
     1.5                     # (tl (tl stack))) env)"
     1.6  
     1.7 -constdefs
     1.8 -  execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val"
     1.9 +definition execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val" where
    1.10    "execute instrs env == hd (exec instrs [] env)"
    1.11  
    1.12