merged
authorblanchet
Fri, 06 Mar 2009 15:54:33 +0100
changeset 30311 66a57e4f043e
parent 30308 23935abfb549 (current diff)
parent 30310 0c1d6621bb19 (diff)
child 30312 0e0cb7ac0281
merged
--- 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