--- a/NEWS Tue Jun 01 15:37:14 2010 +0200
+++ b/NEWS Tue Jun 01 15:38:47 2010 +0200
@@ -435,6 +435,7 @@
"SAT4J_Light". INCOMPATIBILITY.
- Removed "skolemize", "uncurry", "sym_break", "flatten_prop",
"sharing_depth", and "show_skolems" options. INCOMPATIBILITY.
+ - Removed "nitpick_intro" attribute. INCOMPATIBILITY.
* Moved the SMT binding into the HOL image.
--- a/doc-src/Nitpick/nitpick.tex Tue Jun 01 15:37:14 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex Tue Jun 01 15:38:47 2010 +0200
@@ -2578,21 +2578,6 @@
\qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \,=\, u$.
-\flushitem{\textit{nitpick\_intro}}
-
-\nopagebreak
-This attribute specifies the introduction rules of a (co)in\-duc\-tive predicate.
-For predicates defined using the \textbf{inductive} or \textbf{coinductive}
-command, this corresponds to the \textit{intros} rules. The introduction rules
-must be of the form
-
-\qquad $\lbrakk P_1;\> \ldots;\> P_m;\> M~(c\ t_{11}\ \ldots\ t_{1n});\>
-\ldots;\> M~(c\ t_{k1}\ \ldots\ t_{kn})\rbrakk$ \\
-\hbox{}\qquad ${\Longrightarrow}\;\, c\ u_1\ \ldots\ u_n$,
-
-where the $P_i$'s are side conditions that do not involve $c$ and $M$ is an
-optional monotonic operator. The order of the assumptions is irrelevant.
-
\flushitem{\textit{nitpick\_choice\_spec}}
\nopagebreak
@@ -2641,9 +2626,8 @@
``\textit{odd}~$n\,\Longrightarrow\, \textit{odd}~(\textit{Suc}~(\textit{Suc}~n))$''
\postw
-Isabelle automatically attaches the \textit{nitpick\_intro} attribute to
-the above rules. Nitpick then uses the \textit{lfp}-based definition in
-conjunction with these rules. To override this, we can specify an alternative
+By default, Nitpick uses the \textit{lfp}-based definition in conjunction with
+the introduction rules. To override this, we can specify an alternative
definition as follows:
\prew
--- a/src/HOL/HOL.thy Tue Jun 01 15:37:14 2010 +0200
+++ b/src/HOL/HOL.thy Tue Jun 01 15:38:47 2010 +0200
@@ -2033,11 +2033,6 @@
val name = "nitpick_psimp"
val description = "partial equational specification of constants as needed by Nitpick"
)
-structure Nitpick_Intros = Named_Thms
-(
- val name = "nitpick_intro"
- val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
-)
structure Nitpick_Choice_Specs = Named_Thms
(
val name = "nitpick_choice_spec"
@@ -2049,7 +2044,6 @@
Nitpick_Defs.setup
#> Nitpick_Simps.setup
#> Nitpick_Psimps.setup
- #> Nitpick_Intros.setup
#> Nitpick_Choice_Specs.setup
*}
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jun 01 15:37:14 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jun 01 15:38:47 2010 +0200
@@ -1674,10 +1674,14 @@
map (subst_atomic subst o prop_of) (Nitpick_Choice_Specs.get ctxt)
|> const_nondef_table
fun inductive_intro_table ctxt subst def_table =
- def_table_for
- (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt)
- def_table o prop_of)
- o Nitpick_Intros.get) ctxt subst
+ let val thy = ProofContext.theory_of ctxt in
+ def_table_for
+ (maps (map (unfold_mutually_inductive_preds thy def_table o prop_of)
+ o snd o snd)
+ o filter (fn (cat, _) => cat = Spec_Rules.Inductive orelse
+ cat = Spec_Rules.Co_Inductive)
+ o Spec_Rules.get) ctxt subst
+ end
fun ground_theorem_table thy =
fold ((fn @{const Trueprop} $ t1 =>
is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
--- a/src/HOL/Tools/inductive.ML Tue Jun 01 15:37:14 2010 +0200
+++ b/src/HOL/Tools/inductive.ML Tue Jun 01 15:38:47 2010 +0200
@@ -719,8 +719,7 @@
Local_Theory.notes
(map (rec_qualified false) intr_bindings ~~ intr_atts ~~
map (fn th => [([th],
- [Attrib.internal (K (Context_Rules.intro_query NONE)),
- Attrib.internal (K Nitpick_Intros.add)])]) intrs) |>>
+ [Attrib.internal (K (Context_Rules.intro_query NONE))])]) intrs) |>>
map (hd o snd);
val (((_, elims'), (_, [induct'])), lthy2) =
lthy1 |>