# HG changeset patch
# User blanchet
# Date 1235929216 -3600
# Node ID d8944fd4365e6e30e453f49aa50017f9886cdaba
# Parent  e6f76bf0e0673926a713a4bc4314d339c85d8f2f
Added "nitpick_const_def" attribute, for overriding the definition axiom of a constant.

diff -r e6f76bf0e067 -r d8944fd4365e src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Feb 24 16:12:27 2009 +0100
+++ b/src/HOL/HOL.thy	Sun Mar 01 18:40:16 2009 +0100
@@ -1704,6 +1704,11 @@
 subsection {* Nitpick theorem store *}
 
 ML {*
+structure Nitpick_Const_Def_Thms = NamedThmsFun
+(
+  val name = "nitpick_const_def"
+  val description = "pseudo-definition of constants as needed by Nitpick"
+)
 structure Nitpick_Const_Simp_Thms = NamedThmsFun
 (
   val name = "nitpick_const_simp"
@@ -1720,7 +1725,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 *}