equal
deleted
inserted
replaced
1389 by (simp add: tag_def) |
1389 by (simp add: tag_def) |
1390 |
1390 |
1391 |
1391 |
1392 subsection {* Code generator setup *} |
1392 subsection {* Code generator setup *} |
1393 |
1393 |
1394 ML {* |
1394 setup {* |
1395 val _ = |
1395 CodegenTheorems.init_obj ((TrueI, FalseE), (conjI, thm "HOL.atomize_eq" |> Thm.symmetric)) |
1396 let |
|
1397 fun true_tac [] = (ALLGOALS o resolve_tac) [TrueI]; |
|
1398 fun false_tac [false_asm] = (ALLGOALS o resolve_tac) [FalseE] THEN (ALLGOALS o resolve_tac) [false_asm] |
|
1399 fun and_tac impls = (ALLGOALS o resolve_tac) [conjI] |
|
1400 THEN (ALLGOALS o resolve_tac) impls; |
|
1401 fun eq_tac [] = (ALLGOALS o resolve_tac o single |
|
1402 o PureThy.get_thm (the_context ()) o Name) "HOL.atomize_eq"; |
|
1403 in |
|
1404 CodegenTheorems.init_obj (the_context ()) |
|
1405 "bool" ("True", true_tac) ("False", false_tac) |
|
1406 ("op &", and_tac) ("op =", eq_tac) |
|
1407 end; |
|
1408 *} |
1396 *} |
1409 |
1397 |
1410 code_alias |
1398 code_alias |
1411 bool "HOL.bool" |
1399 bool "HOL.bool" |
1412 True "HOL.True" |
1400 True "HOL.True" |