1.1 --- a/src/HOL/HOL.thy	Fri Feb 06 13:43:19 2009 +0100
     1.2 +++ b/src/HOL/HOL.thy	Fri Feb 06 15:57:47 2009 +0100
     1.3 @@ -1701,6 +1701,23 @@
     1.4  *}
     1.5  
     1.6  
     1.7 +subsection {* Nitpick theorem store *}
     1.8 +
     1.9 +ML {*
    1.10 +structure Nitpick_Const_Simps_Thms = NamedThmsFun
    1.11 +(
    1.12 +  val name = "nitpick_const_simps"
    1.13 +  val description = "Equational specification of constants as needed by Nitpick"
    1.14 +)
    1.15 +structure Nitpick_Ind_Intros_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 +)
    1.20 +*}
    1.21 +setup {* Nitpick_Const_Simps_Thms.setup
    1.22 +         o Nitpick_Ind_Intros_Thms.setup *}
    1.23 +
    1.24  subsection {* Legacy tactics and ML bindings *}
    1.25  
    1.26  ML {*