src/HOL/HOL.thy
changeset 30254 7b8afdfa2f83
parent 30242 aea5d7fa7ef5
child 30309 188f0658af9f
     1.1 --- a/src/HOL/HOL.thy	Wed Mar 04 15:49:39 2009 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Mar 04 18:18:05 2009 +0100
     1.3 @@ -1709,6 +1709,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 = "alternative definitions 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 @@ -1725,7 +1730,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