# HG changeset patch
# User blanchet
# Date 1236187085 -3600
# Node ID 7b8afdfa2f8370856bc03651f4f23ffeb642bf09
# Parent  63cae7fd7e64232f3b5b9d2ede1730888cd8bcbd
Second try at adding "nitpick_const_def" attribute.
I don't know what happened the first time (change d8944fd4365e). It just vanished somehow.

diff -r 63cae7fd7e64 -r 7b8afdfa2f83 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Mar 04 15:49:39 2009 +0100
+++ b/src/HOL/HOL.thy	Wed Mar 04 18:18:05 2009 +0100
@@ -1709,6 +1709,11 @@
 subsection {* Nitpick theorem store *}
 
 ML {*
+structure Nitpick_Const_Def_Thms = NamedThmsFun
+(
+  val name = "nitpick_const_def"
+  val description = "alternative definitions of constants as needed by Nitpick"
+)
 structure Nitpick_Const_Simp_Thms = NamedThmsFun
 (
   val name = "nitpick_const_simp"
@@ -1725,7 +1730,8 @@
   val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
 )
 *}
-setup {* Nitpick_Const_Simp_Thms.setup
+setup {* Nitpick_Const_Def_Thms.setup
+         #> Nitpick_Const_Simp_Thms.setup
          #> Nitpick_Const_Psimp_Thms.setup
          #> Nitpick_Ind_Intro_Thms.setup *}