src/HOL/HOL.thy
changeset 29868 787349bb53e9
parent 29866 6e93ae65c678
child 29869 a7a8b90cd882
     1.1 --- a/src/HOL/HOL.thy	Mon Feb 09 10:39:57 2009 +0100
     1.2 +++ b/src/HOL/HOL.thy	Mon Feb 09 12:31:36 2009 +0100
     1.3 @@ -1714,9 +1714,15 @@
     1.4    val name = "nitpick_const_psimp"
     1.5    val description = "Partial equational specification of constants as needed by Nitpick"
     1.6  )
     1.7 +structure Nitpick_Ind_Intro_Thms = NamedThmsFun
     1.8 +(
     1.9 +  val name = "nitpick_ind_intro"
    1.10 +  val description = "Introduction rules for (co)inductive predicates as needed by Nitpick"
    1.11 +)
    1.12  *}
    1.13  setup {* Nitpick_Const_Simp_Thms.setup
    1.14 -         #> Nitpick_Const_Psimp_Thms.setup *}
    1.15 +         #> Nitpick_Const_Psimp_Thms.setup
    1.16 +         #> Nitpick_Ind_Intro_Thms.setup *}
    1.17  
    1.18  subsection {* Legacy tactics and ML bindings *}
    1.19