# HG changeset patch
# User blanchet
# Date 1236349867 -3600
# Node ID 188f0658af9f869ffbdc41971b01a60ee9f79dad
# Parent  381ce8d88cb83fde2c26ab54a514b6fa054fb0f2
Added a "nitpick_maybe" symbol, which is used by Nitpick. This will go away once Nitpick is part of HOL.

diff -r 381ce8d88cb8 -r 188f0658af9f src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Mar 05 10:19:51 2009 +0100
+++ b/src/HOL/HOL.thy	Fri Mar 06 15:31:07 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