1.1 --- a/src/HOL/HOL.thy	Wed Aug 27 04:47:30 2008 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Aug 27 11:24:29 2008 +0200
     1.3 @@ -1659,10 +1659,17 @@
     1.4  
     1.5  subsection {* Code generator basic setup -- see further @{text Code_Setup.thy} *}
     1.6  
     1.7 -code_datatype Trueprop "prop"
     1.8 +setup {*
     1.9 +  Code.map_pre (K HOL_basic_ss)
    1.10 +  #> Code.map_post (K HOL_basic_ss)
    1.11 +*}
    1.12 +
    1.13 +code_datatype True False
    1.14  
    1.15  code_datatype "TYPE('a\<Colon>{})"
    1.16  
    1.17 +code_datatype Trueprop "prop"
    1.18 +
    1.19  lemma Let_case_cert:
    1.20    assumes "CASE \<equiv> (\<lambda>x. Let x f)"
    1.21    shows "CASE x \<equiv> f x"
    1.22 @@ -1718,6 +1725,9 @@
    1.23    shows "\<not> True \<longleftrightarrow> False"
    1.24      and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
    1.25  
    1.26 +lemmas [code func] = Let_def if_True if_False
    1.27 +
    1.28 +lemmas [code func, code unfold, symmetric, code post] = imp_conv_disj
    1.29  
    1.30  
    1.31  subsection {* Legacy tactics and ML bindings *}