Removed "nitpick_maybe" constant. Makarius now taught me a much nicer trick.
authorblanchet
Sat Mar 07 17:05:40 2009 +0100 (2009-03-07)
changeset 30350d9ecd70b1112
parent 30349 110826d1e5ff
child 30351 46aa785d1e29
child 30353 f977e10af7e2
Removed "nitpick_maybe" constant. Makarius now taught me a much nicer trick.
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Sat Mar 07 16:47:36 2009 +0100
     1.2 +++ b/src/HOL/HOL.thy	Sat Mar 07 17:05:40 2009 +0100
     1.3 @@ -1710,8 +1710,6 @@
     1.4  
     1.5  text {* This will be relocated once Nitpick is moved to HOL. *}
     1.6  
     1.7 -consts nitpick_maybe :: "'a \<Rightarrow> 'a" ("_\<^isub>?" [40] 40)
     1.8 -
     1.9  ML {*
    1.10  structure Nitpick_Const_Def_Thms = NamedThmsFun
    1.11  (