--- a/src/HOL/HOL.thy Tue May 09 10:08:20 2006 +0200
+++ b/src/HOL/HOL.thy Tue May 09 10:09:17 2006 +0200
@@ -1391,20 +1391,8 @@
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;
+setup {*
+ CodegenTheorems.init_obj ((TrueI, FalseE), (conjI, thm "HOL.atomize_eq" |> Thm.symmetric))
*}
code_alias