src/HOL/HOL.thy
changeset 30309 188f0658af9f
parent 30254 7b8afdfa2f83
child 30350 d9ecd70b1112
     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