Added "nitpick_const_def" attribute, for overriding the definition axiom of a constant.
1.1 --- a/src/HOL/HOL.thy Tue Feb 24 16:12:27 2009 +0100
1.2 +++ b/src/HOL/HOL.thy Sun Mar 01 18:40:16 2009 +0100
1.3 @@ -1704,6 +1704,11 @@
1.4 subsection {* Nitpick theorem store *}
1.5
1.6 ML {*
1.7 +structure Nitpick_Const_Def_Thms = NamedThmsFun
1.8 +(
1.9 + val name = "nitpick_const_def"
1.10 + val description = "pseudo-definition of constants as needed by Nitpick"
1.11 +)
1.12 structure Nitpick_Const_Simp_Thms = NamedThmsFun
1.13 (
1.14 val name = "nitpick_const_simp"
1.15 @@ -1720,7 +1725,8 @@
1.16 val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
1.17 )
1.18 *}
1.19 -setup {* Nitpick_Const_Simp_Thms.setup
1.20 +setup {* Nitpick_Const_Def_Thms.setup
1.21 + #> Nitpick_Const_Simp_Thms.setup
1.22 #> Nitpick_Const_Psimp_Thms.setup
1.23 #> Nitpick_Ind_Intro_Thms.setup *}
1.24