# HG changeset patch
# User blanchet
# Date 1306485008 -7200
# Node ID cb8d4c2af639c150e5f35ea2bbe4b142aba2b32d
# Parent  7d3ce43d94644b3a5f091e6d46bbf3aefaba9783
update SML section of documentation

diff -r 7d3ce43d9464 -r cb8d4c2af639 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Fri May 27 10:30:08 2011 +0200
+++ b/doc-src/Nitpick/nitpick.tex	Fri May 27 10:30:08 2011 +0200
@@ -2742,10 +2742,12 @@
 
 \prew
 $\textbf{val}\,~\textit{pick\_nits\_in\_term} : \\
-\hbox{}\quad\textit{Proof.state} \rightarrow \textit{params} \rightarrow \textit{bool} \rightarrow \textit{term~list} \rightarrow \textit{term} \\
-\hbox{}\quad{\rightarrow}\; \textit{string} * \textit{Proof.state}$ \\
+\hbox{}\quad\textit{Proof.state} \rightarrow \textit{params} \rightarrow \textit{mode}
+\rightarrow \textit{int} \rightarrow \textit{int} \rightarrow \textit{int}$ \\
+$\hbox{}\quad{\rightarrow}\; (\textit{term} * \textit{term})~\textit{list}
+\rightarrow \textit{term~list} \rightarrow \textit{term} \rightarrow \textit{string} * \textit{Proof.state}$ \\
 $\textbf{val}\,~\textit{pick\_nits\_in\_subgoal} : \\
-\hbox{}\quad\textit{Proof.state} \rightarrow \textit{params} \rightarrow \textit{bool} \rightarrow \textit{int} \rightarrow \textit{string} * \textit{Proof.state}$
+\hbox{}\quad\textit{Proof.state} \rightarrow \textit{params} \rightarrow \textit{mode} \rightarrow \textit{int} \rightarrow \textit{int} \rightarrow \textit{string} * \textit{Proof.state}$
 \postw
 
 The return value is a new proof state paired with an outcome string
@@ -2760,13 +2762,13 @@
 \postw
 
 The second argument lets you override option values before they are parsed and
-put into a \textit{params} record. Here is an example:
+put into a \textit{params} record. Here is an example where Nitpick is invoked
+on subgoal $i$ of $n$ with no time limit:
 
 \prew
 $\textbf{val}\,~\textit{params} = \textit{Nitpick\_Isar.default\_params}~\textit{thy}~[(\textrm{``}\textrm{timeout\/}\textrm{''},\, \textrm{``}\textrm{none}\textrm{''})]$ \\
-$\textbf{val}\,~(\textit{outcome},\, \textit{state}') = \textit{Nitpick.pick\_nits\_in\_subgoal}~\begin{aligned}[t]
-& \textit{state}~\textit{params}~\textit{false} \\[-2pt]
-& \textit{subgoal}\end{aligned}$
+$\textbf{val}\,~(\textit{outcome},\, \textit{state}') = {}$ \\
+$\hbox{}\quad\textit{Nitpick.pick\_nits\_in\_subgoal}~\textit{state}~\textit{params}~\textit{Nitpick.Normal}~\textit{i}~\textit{n}$
 \postw
 
 \let\antiq=\textrm