src/HOL/Code_Setup.thy
changeset 28012 2308843f8b66
parent 27454 fb6a272fe5d0
child 28054 2b84d34c5d02
     1.1 --- a/src/HOL/Code_Setup.thy	Wed Aug 27 04:47:30 2008 +0200
     1.2 +++ b/src/HOL/Code_Setup.thy	Wed Aug 27 11:24:29 2008 +0200
     1.3 @@ -74,7 +74,6 @@
     1.4  
     1.5  subsection {* Generic code generator setup *}
     1.6  
     1.7 -
     1.8  text {* using built-in Haskell equality *}
     1.9  
    1.10  code_class eq
    1.11 @@ -86,8 +85,6 @@
    1.12  
    1.13  text {* type bool *}
    1.14  
    1.15 -lemmas [code func, code unfold, symmetric, code post] = imp_conv_disj
    1.16 -
    1.17  code_type bool
    1.18    (SML "bool")
    1.19    (OCaml "bool")
    1.20 @@ -113,17 +110,14 @@
    1.21  
    1.22  text {* code generation for undefined as exception *}
    1.23  
    1.24 +code_abort undefined
    1.25 +
    1.26  code_const undefined
    1.27    (SML "raise/ Fail/ \"undefined\"")
    1.28    (OCaml "failwith/ \"undefined\"")
    1.29    (Haskell "error/ \"undefined\"")
    1.30  
    1.31  
    1.32 -text {* Let and If *}
    1.33 -
    1.34 -lemmas [code func] = Let_def if_True if_False
    1.35 -
    1.36 -
    1.37  subsection {* Evaluation oracle *}
    1.38  
    1.39  ML {*