adapted for definitional code generation

--- a/src/HOL/Datatype.thy	Thu Apr 06 16:10:46 2006 +0200
+++ b/src/HOL/Datatype.thy	Thu Apr 06 16:11:30 2006 +0200
@@ -222,31 +222,31 @@
 
 subsubsection {* Codegenerator setup *}
 
-lemma [code]:
+lemma [code fun]:
   "(\<not> True) = False" by (rule HOL.simp_thms)
 
-lemma [code]:
+lemma [code fun]:
   "(\<not> False) = True" by (rule HOL.simp_thms)
 
-lemma [code]:
+lemma [code fun]:
   shows "(False \<and> x) = False"
   and   "(True \<and> x) = x"
   and   "(x \<and> False) = False"
   and   "(x \<and> True) = x" by simp_all
 
-lemma [code]:
+lemma [code fun]:
   shows "(False \<or> x) = x"
   and   "(True \<or> x) = True"
   and   "(x \<or> False) = x"
   and   "(x \<or> True) = True" by simp_all
 
 declare
-  if_True [code]
-  if_False [code]
+  if_True [code fun]
+  if_False [code fun]
   fst_conv [code]
   snd_conv [code]
 
-lemma [code unfold]:
+lemma [code unfolt]:
   "1 == Suc 0" by simp
 
 code_generate True False Not "op &" "op |" If

--- a/src/HOL/HOL.thy	Thu Apr 06 16:10:46 2006 +0200
+++ b/src/HOL/HOL.thy	Thu Apr 06 16:11:30 2006 +0200
@@ -1399,6 +1399,22 @@
 
 subsection {* Code generator setup *}
 
+ML {*
+val _ =
+  let
+    fun true_tac [] = (ALLGOALS o resolve_tac) [TrueI];
+    fun false_tac [false_asm] = (ALLGOALS o resolve_tac) [FalseE] THEN (ALLGOALS o resolve_tac) [false_asm]
+    fun and_tac impls = (ALLGOALS o resolve_tac) [conjI]
+        THEN (ALLGOALS o resolve_tac) impls;
+    fun eq_tac [] = (ALLGOALS o resolve_tac o single
+      o PureThy.get_thm (the_context ()) o Name) "HOL.atomize_eq";
+  in
+    CodegenTheorems.init_obj (the_context ())
+      "bool" ("True", true_tac) ("False", false_tac)
+        ("op &", and_tac) ("op =", eq_tac)
+  end;
+*}
+
 code_alias
   bool "HOL.bool"
   True "HOL.True"