Added a "nitpick_maybe" symbol, which is used by Nitpick. This will go away once Nitpick is part of HOL.
1.1 --- a/src/HOL/HOL.thy Thu Mar 05 10:19:51 2009 +0100
1.2 +++ b/src/HOL/HOL.thy Fri Mar 06 15:31:07 2009 +0100
1.3 @@ -1706,7 +1706,11 @@
1.4 *}
1.5
1.6
1.7 -subsection {* Nitpick theorem store *}
1.8 +subsection {* Nitpick hooks *}
1.9 +
1.10 +text {* This will be relocated once Nitpick is moved to HOL. *}
1.11 +
1.12 +consts nitpick_maybe :: "'a \<Rightarrow> 'a" ("_\<^isub>?" [40] 40)
1.13
1.14 ML {*
1.15 structure Nitpick_Const_Def_Thms = NamedThmsFun