--- a/src/HOL/HOL.thy Tue Mar 16 08:45:08 2010 +0100
+++ b/src/HOL/HOL.thy Wed Mar 17 09:14:43 2010 +0100
@@ -1999,8 +1999,6 @@
subsubsection {* Nitpick setup *}
-text {* This will be relocated once Nitpick is moved to HOL. *}
-
ML {*
structure Nitpick_Defs = Named_Thms
(
@@ -2022,6 +2020,11 @@
val name = "nitpick_intro"
val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
)
+structure Nitpick_Choice_Specs = Named_Thms
+(
+ val name = "nitpick_choice_specs"
+ val description = "choice specification of constants as needed by Nitpick"
+)
*}
setup {*
@@ -2029,6 +2032,7 @@
#> Nitpick_Simps.setup
#> Nitpick_Psimps.setup
#> Nitpick_Intros.setup
+ #> Nitpick_Choice_Specs.setup
*}