--- a/src/HOL/Code_Setup.thy Wed Aug 27 04:47:30 2008 +0200
+++ b/src/HOL/Code_Setup.thy Wed Aug 27 11:24:29 2008 +0200
@@ -74,7 +74,6 @@
subsection {* Generic code generator setup *}
-
text {* using built-in Haskell equality *}
code_class eq
@@ -86,8 +85,6 @@
text {* type bool *}
-lemmas [code func, code unfold, symmetric, code post] = imp_conv_disj
-
code_type bool
(SML "bool")
(OCaml "bool")
@@ -113,17 +110,14 @@
text {* code generation for undefined as exception *}
+code_abort undefined
+
code_const undefined
(SML "raise/ Fail/ \"undefined\"")
(OCaml "failwith/ \"undefined\"")
(Haskell "error/ \"undefined\"")
-text {* Let and If *}
-
-lemmas [code func] = Let_def if_True if_False
-
-
subsection {* Evaluation oracle *}
ML {*
--- a/src/HOL/HOL.thy Wed Aug 27 04:47:30 2008 +0200
+++ b/src/HOL/HOL.thy Wed Aug 27 11:24:29 2008 +0200
@@ -1659,10 +1659,17 @@
subsection {* Code generator basic setup -- see further @{text Code_Setup.thy} *}
-code_datatype Trueprop "prop"
+setup {*
+ Code.map_pre (K HOL_basic_ss)
+ #> Code.map_post (K HOL_basic_ss)
+*}
+
+code_datatype True False
code_datatype "TYPE('a\<Colon>{})"
+code_datatype Trueprop "prop"
+
lemma Let_case_cert:
assumes "CASE \<equiv> (\<lambda>x. Let x f)"
shows "CASE x \<equiv> f x"
@@ -1718,6 +1725,9 @@
shows "\<not> True \<longleftrightarrow> False"
and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
+lemmas [code func] = Let_def if_True if_False
+
+lemmas [code func, code unfold, symmetric, code post] = imp_conv_disj
subsection {* Legacy tactics and ML bindings *}