diff -r 7ae51d5ea05d -r 9edc2bd6d2bd doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Mon Feb 22 14:36:10 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Mon Feb 22 19:31:00 2010 +0100
@@ -141,11 +141,11 @@
 
 This section introduces Nitpick by presenting small examples. If possible, you
 should try out the examples on your workstation. Your theory file should start
-the standard way:
+as follows:
 
 \prew
 \textbf{theory}~\textit{Scratch} \\
-\textbf{imports}~\textit{Main} \\
+\textbf{imports}~\textit{Main~Coinductive\_List~Quotient\_Product~RealDef} \\
 \textbf{begin}
 \postw
 
@@ -439,7 +439,7 @@
 value (displayed as `$\unk$'). The type \textit{int} is handled similarly.
 Internally, undefined values lead to a three-valued logic.
 
-Here is an example involving \textit{int}:
+Here is an example involving \textit{int\/}:
 
 \prew
 \textbf{lemma} ``$\lbrakk i \le j;\> n \le (m{\Colon}\mathit{int})\rbrakk \,\Longrightarrow\, i * n + j * m \le i * m + j * n$'' \\
@@ -627,7 +627,7 @@
 genuine counterexample for \textit{card}~$'a~\textit{list}$~= 10, it is very
 unlikely that one could be found for smaller cardinalities.
 
-\subsection{Typedefs, Records, Rationals, and Reals}
+\subsection{Typedefs, Quotient Types, Records, Rationals, and Reals}
 \label{typedefs-records-rationals-and-reals}
 
 Nitpick generally treats types declared using \textbf{typedef} as datatypes
@@ -651,12 +651,41 @@
 \hbox{}\qquad\qquad $\textit{three} = \{\Abs{0},\, \Abs{1},\, \Abs{2},\, \unr\}$
 \postw
 
-%% MARK
 In the output above, $\Abs{n}$ abbreviates $\textit{Abs\_three}~n$.
 
-%% MARK
-Records, which are implemented as \textbf{typedef}s behind the scenes, are
-handled in much the same way:
+Quotient types are handled in much the same way. The following fragment defines
+the integer type \textit{my\_int} by encoding the integer $x$ by a pair of
+natural numbers $(m, n)$ such that $x + n = m$:
+
+\prew
+\textbf{fun} \textit{my\_int\_rel} \textbf{where} \\
+``$\textit{my\_int\_rel}~(x,\, y)~(u,\, v) = (x + v = u + y)$'' \\[2\smallskipamount]
+%
+\textbf{quotient\_type}~\textit{my\_int} = ``$\textit{nat} \times \textit{nat\/}$''$\;{/}\;$\textit{my\_int\_rel} \\
+\textbf{by}~(\textit{auto simp add\/}:\ \textit{equivp\_def expand\_fun\_eq}) \\[2\smallskipamount]
+%
+\textbf{definition}~\textit{add\_raw}~\textbf{where} \\
+``$\textit{add\_raw} \,\equiv\, \lambda(x,\, y)~(u,\, v).\; (x + (u\Colon\textit{nat}), y + (v\Colon\textit{nat}))$'' \\[2\smallskipamount]
+%
+\textbf{quotient\_definition} ``$\textit{add\/}\Colon\textit{my\_int} \Rightarrow \textit{my\_int} \Rightarrow \textit{my\_int\/}$'' \textbf{is} \textit{add\_raw} \\[2\smallskipamount]
+%
+\textbf{lemma} ``$\textit{add}~x~y = \textit{add}~x~x$'' \\
+\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
+\slshape Nitpick found a counterexample: \\[2\smallskipamount]
+\hbox{}\qquad Free variables: \nopagebreak \\
+\hbox{}\qquad\qquad $x = \Abs{(0,\, 0)}$ \\
+\hbox{}\qquad\qquad $y = \Abs{(1,\, 0)}$ \\
+\hbox{}\qquad Datatypes: \\
+\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, \unr\}$ \\
+\hbox{}\qquad\qquad $\textit{nat} \times \textit{nat} = \{(0,\, 0),\> (1,\, 0),\> \unr\}$ \\
+\hbox{}\qquad\qquad $\textit{my\_int} = \{\Abs{(0,\, 0)},\> \Abs{(1,\, 0)},\> \unr\}$
+\postw
+
+In the counterexample, $\Abs{(0,\, 0)}$ and $\Abs{(1,\, 0)}$ represent the
+integers $0$ and $1$, respectively. Other representants would have been
+possible---e.g., $\Abs{(5,\, 5)}$ and $\Abs{(12,\, 11)}$.
+
+Records are also handled as datatypes with a single constructor:
 
 \prew
 \textbf{record} \textit{point} = \\
@@ -675,6 +704,8 @@
 & \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr,\, \unr\}\end{aligned}$
 \postw
 
+
+
 Finally, Nitpick provides rudimentary support for rationals and reals using a
 similar approach:
 
@@ -949,13 +980,13 @@
 \slshape The type ``\kern1pt$'a$'' passed the monotonicity test. Nitpick might be able to skip
 some scopes. \\[2\smallskipamount]
 Trying 8 scopes: \\
-\hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} ``\kern1pt$'a~\textit{list}$''~= 1,
+\hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 1,
 and \textit{bisim\_depth}~= 0. \\
 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
-\hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} ``\kern1pt$'a~\textit{list}$''~= 8,
+\hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 8,
 and \textit{bisim\_depth}~= 7. \\[2\smallskipamount]
 Nitpick found a counterexample for {\itshape card}~$'a$ = 2,
-\textit{card}~``\kern1pt$'a~\textit{list}$''~= 2, and \textit{bisim\_\allowbreak
+\textit{card}~``\kern1pt$'a~\textit{list\/}$''~= 2, and \textit{bisim\_\allowbreak
 depth}~= 1:
 \\[2\smallskipamount]
 \hbox{}\qquad Free variables: \nopagebreak \\
@@ -1118,7 +1149,7 @@
 \textit{Lam}~(\textit{Lam}~(\textit{Var}~0))$. Using the traditional
 $\lambda$-term notation, $t$~is
 $\lambda x\, y.\> x$ whereas $\textit{subst}~\sigma~t$ is $\lambda x\, y.\> y$.
-The bug is in \textit{subst}: The $\textit{lift}~(\sigma~m)~1$ call should be
+The bug is in \textit{subst\/}: The $\textit{lift}~(\sigma~m)~1$ call should be
 replaced with $\textit{lift}~(\sigma~m)~0$.
 
 An interesting aspect of Nitpick's verbose output is that it assigned inceasing
@@ -1509,7 +1540,7 @@
 completeness of the set $S$. First, soundness:
 
 \prew
-\textbf{theorem}~\textit{S\_sound}: \\
+\textbf{theorem}~\textit{S\_sound\/}: \\
 ``$w \in S \longrightarrow \textit{length}~[x\mathbin{\leftarrow} w.\; x = a] =
   \textit{length}~[x\mathbin{\leftarrow} w.\; x = b]$'' \\
 \textbf{nitpick} \\[2\smallskipamount]
@@ -1691,7 +1722,7 @@
 of elements stored in the tree:
 
 \prew
-\textbf{theorem}~\textit{dataset\_skew\_split}:\\
+\textbf{theorem}~\textit{dataset\_skew\_split\/}:\\
 ``$\textit{dataset}~(\textit{skew}~t) = \textit{dataset}~t$'' \\
 ``$\textit{dataset}~(\textit{split}~t) = \textit{dataset}~t$'' \\
 \textbf{nitpick} \\[2\smallskipamount]
@@ -1702,7 +1733,7 @@
 should not alter the tree:
 
 \prew
-\textbf{theorem}~\textit{wf\_skew\_split}:\\
+\textbf{theorem}~\textit{wf\_skew\_split\/}:\\
 ``$\textit{wf}~t\,\Longrightarrow\, \textit{skew}~t = t$'' \\
 ``$\textit{wf}~t\,\Longrightarrow\, \textit{split}~t = t$'' \\
 \textbf{nitpick} \\[2\smallskipamount]
@@ -1723,7 +1754,7 @@
 \textit{split}. Let's see if this causes any problems:
 
 \prew
-\textbf{theorem}~\textit{wf\_insort}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
+\textbf{theorem}~\textit{wf\_insort\/}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
 \textbf{nitpick} \\[2\smallskipamount]
 \slshape Nitpick found a counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
 \hbox{}\qquad Free variables: \nopagebreak \\
@@ -1738,7 +1769,7 @@
 $\textit{insort}~t~x$ using the \textit{eval} option. This gives
 
 \prew
-\textbf{theorem} \textit{wf\_insort\_nat}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~(x\Colon\textit{nat}))$'' \\
+\textbf{theorem} \textit{wf\_insort\_nat\/}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~(x\Colon\textit{nat}))$'' \\
 \textbf{nitpick} [\textit{eval} = ``$\textit{insort}~t~x$''] \\[2\smallskipamount]
 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
 \hbox{}\qquad Free variables: \nopagebreak \\
@@ -1755,7 +1786,7 @@
 Reintroducing the code seems to solve the problem:
 
 \prew
-\textbf{theorem}~\textit{wf\_insort}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
+\textbf{theorem}~\textit{wf\_insort\/}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
 \textbf{nitpick} \\[2\smallskipamount]
 {\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
 \postw
@@ -1764,7 +1795,7 @@
 obvious way:
 
 \prew
-\textbf{theorem} \textit{dataset\_insort}:\kern.4em
+\textbf{theorem} \textit{dataset\_insort\/}:\kern.4em
 ``$\textit{dataset}~(\textit{insort}~t~x) = \{x\} \cup \textit{dataset}~t$'' \\
 \textbf{nitpick} \\[2\smallskipamount]
 {\slshape Nitpick ran out of time after checking 6 of 8 scopes.}
@@ -1825,19 +1856,19 @@
 
 \begin{enum}
 \item[$\bullet$] \qtybf{string}: A string.
-\item[$\bullet$] \qtybf{bool}: \textit{true} or \textit{false}.
-\item[$\bullet$] \qtybf{bool\_or\_smart}: \textit{true}, \textit{false}, or \textit{smart}.
-\item[$\bullet$] \qtybf{int}: An integer. Negative integers are prefixed with a hyphen.
-\item[$\bullet$] \qtybf{int\_or\_smart}: An integer or \textit{smart}.
+\item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.
+\item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or \textit{smart}.
+\item[$\bullet$] \qtybf{int\/}: An integer. Negative integers are prefixed with a hyphen.
+\item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}.
 \item[$\bullet$] \qtybf{int\_range}: An integer (e.g., 3) or a range
 of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\<midarrow\char`\>}.
 
 \item[$\bullet$] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8).
 \item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes), $s$ (seconds), or \textit{ms}
 (milliseconds), or the keyword \textit{none} ($\infty$ years).
-\item[$\bullet$] \qtybf{const}: The name of a HOL constant.
+\item[$\bullet$] \qtybf{const\/}: The name of a HOL constant.
 \item[$\bullet$] \qtybf{term}: A HOL term (e.g., ``$f~x$'').
-\item[$\bullet$] \qtybf{term\_list}: A space-separated list of HOL terms (e.g.,
+\item[$\bullet$] \qtybf{term\_list\/}: A space-separated list of HOL terms (e.g.,
 ``$f~x$''~``$g~y$'').
 \item[$\bullet$] \qtybf{type}: A HOL type.
 \end{enum}
@@ -2190,7 +2221,6 @@
 the \textit{format}~\qty{term} option described above.
 \end{enum}
 
-%% MARK: Authentication
 \subsection{Authentication}
 \label{authentication}
 
@@ -2564,14 +2594,14 @@
 definition as follows:
 
 \prew
-\textbf{lemma} $\mathit{odd\_def}'$ [\textit{nitpick\_def}]: ``$\textit{odd}~n \,\equiv\, n~\textrm{mod}~2 = 1$''
+\textbf{lemma} $\mathit{odd\_def}'$ [\textit{nitpick\_def}]:\kern.4em ``$\textit{odd}~n \,\equiv\, n~\textrm{mod}~2 = 1$''
 \postw
 
 Nitpick then expands all occurrences of $\mathit{odd}~n$ to $n~\textrm{mod}~2
 = 1$. Alternatively, we can specify an equational specification of the constant:
 
 \prew
-\textbf{lemma} $\mathit{odd\_simp}'$ [\textit{nitpick\_simp}]: ``$\textit{odd}~n = (n~\textrm{mod}~2 = 1)$''
+\textbf{lemma} $\mathit{odd\_simp}'$ [\textit{nitpick\_simp}]:\kern.4em ``$\textit{odd}~n = (n~\textrm{mod}~2 = 1)$''
 \postw
 
 Such tweaks should be done with great care, because Nitpick will assume that the