src/HOL/HOL.thy
changeset 30350 d9ecd70b1112
parent 30309 188f0658af9f
child 30609 983e8b6e4e69
     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  (