# HG changeset patch
# User blanchet
# Date 1233932267 -3600
# Node ID dadad1831e9dc5933a3f955add14d36ba6a61c80
# Parent  07f53494cf2075be4d823d8ab59b24094e3bf11d
Added "nitpick_const_simps" and "nitpick_ind_intros" attributes for theorems;
these will be used by Nitpick, which will be released independently of Isabelle
2009, but they need to be in.

diff -r 07f53494cf20 -r dadad1831e9d src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Feb 06 13:43:19 2009 +0100
+++ b/src/HOL/HOL.thy	Fri Feb 06 15:57:47 2009 +0100
@@ -1701,6 +1701,23 @@
 *}
 
 
+subsection {* Nitpick theorem store *}
+
+ML {*
+structure Nitpick_Const_Simps_Thms = NamedThmsFun
+(
+  val name = "nitpick_const_simps"
+  val description = "Equational specification of constants as needed by Nitpick"
+)
+structure Nitpick_Ind_Intros_Thms = NamedThmsFun
+(
+  val name = "nitpick_ind_intros"
+  val description = "Introduction rules for inductive predicate as needed by Nitpick"
+)
+*}
+setup {* Nitpick_Const_Simps_Thms.setup
+         o Nitpick_Ind_Intros_Thms.setup *}
+
 subsection {* Legacy tactics and ML bindings *}
 
 ML {*
diff -r 07f53494cf20 -r dadad1831e9d src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Feb 06 13:43:19 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Feb 06 15:57:47 2009 +0100
@@ -42,7 +42,8 @@
 
 fun add_simps fnames post sort extra_qualify label moreatts simps lthy =
     let
-      val atts = Attrib.internal (K Simplifier.simp_add) :: moreatts
+      val atts = Attrib.internal (K Simplifier.simp_add) ::
+                 Attrib.internal (K Nitpick_Const_Simps_Thms.add) :: moreatts
       val spec = post simps
                    |> map (apfst (apsnd (append atts)))
                    |> map (apfst (apfst extra_qualify))
diff -r 07f53494cf20 -r dadad1831e9d src/HOL/Tools/function_package/size.ML
--- a/src/HOL/Tools/function_package/size.ML	Fri Feb 06 13:43:19 2009 +0100
+++ b/src/HOL/Tools/function_package/size.ML	Fri Feb 06 15:57:47 2009 +0100
@@ -209,8 +209,9 @@
 
     val ([size_thms], thy'') =  PureThy.add_thmss
       [((Binding.name "size", size_eqns),
-        [Simplifier.simp_add, Thm.declaration_attribute
-              (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
+        [Simplifier.simp_add, Nitpick_Const_Simps_Thms.add,
+         Thm.declaration_attribute
+             (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
 
   in
     SizeData.map (fold (Symtab.update_new o apsnd (rpair size_thms))
diff -r 07f53494cf20 -r dadad1831e9d src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri Feb 06 13:43:19 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Fri Feb 06 15:57:47 2009 +0100
@@ -691,7 +691,8 @@
       ctxt |>
       LocalTheory.notes kind
         (map rec_qualified intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
-           [Attrib.internal (K (ContextRules.intro_query NONE))])]) intrs) |>>
+           [Attrib.internal (K (ContextRules.intro_query NONE)),
+            Attrib.internal (K Nitpick_Ind_Intros_Thms.add)])]) intrs) |>>
       map (hd o snd);
     val (((_, elims'), (_, [induct'])), ctxt2) =
       ctxt1 |>
diff -r 07f53494cf20 -r dadad1831e9d src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Fri Feb 06 13:43:19 2009 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Fri Feb 06 15:57:47 2009 +0100
@@ -251,7 +251,8 @@
       (space_implode "_" (map (Sign.base_name o #1) defs));
     val spec' = (map o apfst o apfst) qualify spec;
     val simp_atts = map (Attrib.internal o K)
-      [Simplifier.simp_add, Code.add_default_eqn_attribute];
+      [Simplifier.simp_add, Code.add_default_eqn_attribute,
+       Nitpick_Const_Simps_Thms.add];
   in
     lthy
     |> set_group ? LocalTheory.set_group (serial_string ())