1.1 --- a/src/HOL/Datatype.thy	Thu Apr 06 16:10:46 2006 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Thu Apr 06 16:11:30 2006 +0200
     1.3 @@ -222,31 +222,31 @@
     1.4  
     1.5  subsubsection {* Codegenerator setup *}
     1.6  
     1.7 -lemma [code]:
     1.8 +lemma [code fun]:
     1.9    "(\<not> True) = False" by (rule HOL.simp_thms)
    1.10  
    1.11 -lemma [code]:
    1.12 +lemma [code fun]:
    1.13    "(\<not> False) = True" by (rule HOL.simp_thms)
    1.14  
    1.15 -lemma [code]:
    1.16 +lemma [code fun]:
    1.17    shows "(False \<and> x) = False"
    1.18    and   "(True \<and> x) = x"
    1.19    and   "(x \<and> False) = False"
    1.20    and   "(x \<and> True) = x" by simp_all
    1.21  
    1.22 -lemma [code]:
    1.23 +lemma [code fun]:
    1.24    shows "(False \<or> x) = x"
    1.25    and   "(True \<or> x) = True"
    1.26    and   "(x \<or> False) = x"
    1.27    and   "(x \<or> True) = True" by simp_all
    1.28  
    1.29  declare
    1.30 -  if_True [code]
    1.31 -  if_False [code]
    1.32 +  if_True [code fun]
    1.33 +  if_False [code fun]
    1.34    fst_conv [code]
    1.35    snd_conv [code]
    1.36  
    1.37 -lemma [code unfold]:
    1.38 +lemma [code unfolt]:
    1.39    "1 == Suc 0" by simp
    1.40  
    1.41  code_generate True False Not "op &" "op |" If

     2.1 --- a/src/HOL/HOL.thy	Thu Apr 06 16:10:46 2006 +0200
     2.2 +++ b/src/HOL/HOL.thy	Thu Apr 06 16:11:30 2006 +0200
     2.3 @@ -1399,6 +1399,22 @@
     2.4  
     2.5  subsection {* Code generator setup *}
     2.6  
     2.7 +ML {*
     2.8 +val _ =
     2.9 +  let
    2.10 +    fun true_tac [] = (ALLGOALS o resolve_tac) [TrueI];
    2.11 +    fun false_tac [false_asm] = (ALLGOALS o resolve_tac) [FalseE] THEN (ALLGOALS o resolve_tac) [false_asm]
    2.12 +    fun and_tac impls = (ALLGOALS o resolve_tac) [conjI]
    2.13 +        THEN (ALLGOALS o resolve_tac) impls;
    2.14 +    fun eq_tac [] = (ALLGOALS o resolve_tac o single
    2.15 +      o PureThy.get_thm (the_context ()) o Name) "HOL.atomize_eq";
    2.16 +  in
    2.17 +    CodegenTheorems.init_obj (the_context ())
    2.18 +      "bool" ("True", true_tac) ("False", false_tac)
    2.19 +        ("op &", and_tac) ("op =", eq_tac)
    2.20 +  end;
    2.21 +*}
    2.22 +
    2.23  code_alias
    2.24    bool "HOL.bool"
    2.25    True "HOL.True"