1.1 --- a/doc-src/Nitpick/nitpick.tex	Tue Jun 01 15:37:14 2010 +0200
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Tue Jun 01 15:38:47 2010 +0200
     1.3 @@ -2578,21 +2578,6 @@
     1.4  
     1.5  \qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \,=\, u$.
     1.6  
     1.7 -\flushitem{\textit{nitpick\_intro}}
     1.8 -
     1.9 -\nopagebreak
    1.10 -This attribute specifies the introduction rules of a (co)in\-duc\-tive predicate.
    1.11 -For predicates defined using the \textbf{inductive} or \textbf{coinductive}
    1.12 -command, this corresponds to the \textit{intros} rules. The introduction rules
    1.13 -must be of the form
    1.14 -
    1.15 -\qquad $\lbrakk P_1;\> \ldots;\> P_m;\> M~(c\ t_{11}\ \ldots\ t_{1n});\>
    1.16 -\ldots;\> M~(c\ t_{k1}\ \ldots\ t_{kn})\rbrakk$ \\
    1.17 -\hbox{}\qquad ${\Longrightarrow}\;\, c\ u_1\ \ldots\ u_n$,
    1.18 -
    1.19 -where the $P_i$'s are side conditions that do not involve $c$ and $M$ is an
    1.20 -optional monotonic operator. The order of the assumptions is irrelevant.
    1.21 -
    1.22  \flushitem{\textit{nitpick\_choice\_spec}}
    1.23  
    1.24  \nopagebreak
    1.25 @@ -2641,9 +2626,8 @@
    1.26  ``\textit{odd}~$n\,\Longrightarrow\, \textit{odd}~(\textit{Suc}~(\textit{Suc}~n))$''
    1.27  \postw
    1.28  
    1.29 -Isabelle automatically attaches the \textit{nitpick\_intro} attribute to
    1.30 -the above rules. Nitpick then uses the \textit{lfp}-based definition in
    1.31 -conjunction with these rules. To override this, we can specify an alternative
    1.32 +By default, Nitpick uses the \textit{lfp}-based definition in conjunction with
    1.33 +the introduction rules. To override this, we can specify an alternative
    1.34  definition as follows:
    1.35  
    1.36  \prew