1.1 --- a/src/HOL/HOL.thy Fri Feb 06 16:00:05 2009 +0100
1.2 +++ b/src/HOL/HOL.thy Mon Feb 09 10:37:59 2009 +0100
1.3 @@ -1704,19 +1704,19 @@
1.4 subsection {* Nitpick theorem store *}
1.5
1.6 ML {*
1.7 -structure Nitpick_Const_Simps_Thms = NamedThmsFun
1.8 +structure Nitpick_Const_Simp_Thms = NamedThmsFun
1.9 (
1.10 - val name = "nitpick_const_simps"
1.11 + val name = "nitpick_const_simp"
1.12 val description = "Equational specification of constants as needed by Nitpick"
1.13 )
1.14 -structure Nitpick_Ind_Intros_Thms = NamedThmsFun
1.15 +structure Nitpick_Const_Psimp_Thms = NamedThmsFun
1.16 (
1.17 - val name = "nitpick_ind_intros"
1.18 - val description = "Introduction rules for inductive predicate as needed by Nitpick"
1.19 + val name = "nitpick_const_psimp"
1.20 + val description = "Partial equational specification of constants as needed by Nitpick"
1.21 )
1.22 *}
1.23 -setup {* Nitpick_Const_Simps_Thms.setup
1.24 - o Nitpick_Ind_Intros_Thms.setup *}
1.25 +setup {* Nitpick_Const_Simp_Thms.setup
1.26 + #> Nitpick_Const_Psimp_Thms.setup *}
1.27
1.28 subsection {* Legacy tactics and ML bindings *}
1.29