author | blanchet |
Fri, 06 Mar 2009 15:54:33 +0100 | |
changeset 30311 | 66a57e4f043e |
parent 30308 | 23935abfb549 (current diff) |
parent 30310 | 0c1d6621bb19 (diff) |
child 30312 | 0e0cb7ac0281 |
--- a/src/HOL/HOL.thy Fri Mar 06 15:51:18 2009 +0100 +++ b/src/HOL/HOL.thy Fri Mar 06 15:54:33 2009 +0100 @@ -1706,7 +1706,11 @@ *} -subsection {* Nitpick theorem store *} +subsection {* Nitpick hooks *} + +text {* This will be relocated once Nitpick is moved to HOL. *} + +consts nitpick_maybe :: "'a \<Rightarrow> 'a" ("_\<^isub>?" [40] 40) ML {* structure Nitpick_Const_Def_Thms = NamedThmsFun