equal
deleted
inserted
replaced
1704 #> Codegen.setup |
1704 #> Codegen.setup |
1705 #> RecfunCodegen.setup |
1705 #> RecfunCodegen.setup |
1706 *} |
1706 *} |
1707 |
1707 |
1708 |
1708 |
1709 subsection {* Nitpick theorem store *} |
1709 subsection {* Nitpick hooks *} |
|
1710 |
|
1711 text {* This will be relocated once Nitpick is moved to HOL. *} |
|
1712 |
|
1713 consts nitpick_maybe :: "'a \<Rightarrow> 'a" ("_\<^isub>?" [40] 40) |
1710 |
1714 |
1711 ML {* |
1715 ML {* |
1712 structure Nitpick_Const_Def_Thms = NamedThmsFun |
1716 structure Nitpick_Const_Def_Thms = NamedThmsFun |
1713 ( |
1717 ( |
1714 val name = "nitpick_const_def" |
1718 val name = "nitpick_const_def" |