--- a/src/HOL/HOL.thy Mon Feb 09 10:39:57 2009 +0100
+++ b/src/HOL/HOL.thy Mon Feb 09 12:31:36 2009 +0100
@@ -1714,9 +1714,15 @@
val name = "nitpick_const_psimp"
val description = "Partial equational specification of constants as needed by Nitpick"
)
+structure Nitpick_Ind_Intro_Thms = NamedThmsFun
+(
+ val name = "nitpick_ind_intro"
+ val description = "Introduction rules for (co)inductive predicates as needed by Nitpick"
+)
*}
setup {* Nitpick_Const_Simp_Thms.setup
- #> Nitpick_Const_Psimp_Thms.setup *}
+ #> Nitpick_Const_Psimp_Thms.setup
+ #> Nitpick_Ind_Intro_Thms.setup *}
subsection {* Legacy tactics and ML bindings *}