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 {*

     2.1 --- a/src/HOL/HOL.thy	Wed Aug 27 04:47:30 2008 +0200
     2.2 +++ b/src/HOL/HOL.thy	Wed Aug 27 11:24:29 2008 +0200
     2.3 @@ -1659,10 +1659,17 @@
     2.4  
     2.5  subsection {* Code generator basic setup -- see further @{text Code_Setup.thy} *}
     2.6  
     2.7 -code_datatype Trueprop "prop"
     2.8 +setup {*
     2.9 +  Code.map_pre (K HOL_basic_ss)
    2.10 +  #> Code.map_post (K HOL_basic_ss)
    2.11 +*}
    2.12 +
    2.13 +code_datatype True False
    2.14  
    2.15  code_datatype "TYPE('a\<Colon>{})"
    2.16  
    2.17 +code_datatype Trueprop "prop"
    2.18 +
    2.19  lemma Let_case_cert:
    2.20    assumes "CASE \<equiv> (\<lambda>x. Let x f)"
    2.21    shows "CASE x \<equiv> f x"
    2.22 @@ -1718,6 +1725,9 @@
    2.23    shows "\<not> True \<longleftrightarrow> False"
    2.24      and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
    2.25  
    2.26 +lemmas [code func] = Let_def if_True if_False
    2.27 +
    2.28 +lemmas [code func, code unfold, symmetric, code post] = imp_conv_disj
    2.29  
    2.30  
    2.31  subsection {* Legacy tactics and ML bindings *}