1.1 --- a/doc-src/Nitpick/nitpick.tex	Thu Feb 04 16:50:26 2010 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Fri Feb 05 11:14:34 2010 +0100
     1.3 @@ -1694,7 +1694,7 @@
     1.4  ``$\textit{dataset}~(\textit{skew}~t) = \textit{dataset}~t$'' \\
     1.5  ``$\textit{dataset}~(\textit{split}~t) = \textit{dataset}~t$'' \\
     1.6  \textbf{nitpick} \\[2\smallskipamount]
     1.7 -{\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
     1.8 +{\slshape Nitpick found no counterexample.}
     1.9  \postw
    1.10  
    1.11  Furthermore, applying \textit{skew} or \textit{split} to a well-formed tree
    1.12 @@ -1756,7 +1756,7 @@
    1.13  \prew
    1.14  \textbf{theorem}~\textit{wf\_insort}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
    1.15  \textbf{nitpick} \\[2\smallskipamount]
    1.16 -{\slshape Nitpick ran out of time after checking 6 of 8 scopes.}
    1.17 +{\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
    1.18  \postw
    1.19  
    1.20  Insertion should transform the set of elements represented by the tree in the
    1.21 @@ -1766,14 +1766,14 @@
    1.22  \textbf{theorem} \textit{dataset\_insort}:\kern.4em
    1.23  ``$\textit{dataset}~(\textit{insort}~t~x) = \{x\} \cup \textit{dataset}~t$'' \\
    1.24  \textbf{nitpick} \\[2\smallskipamount]
    1.25 -{\slshape Nitpick ran out of time after checking 5 of 8 scopes.}
    1.26 +{\slshape Nitpick ran out of time after checking 6 of 8 scopes.}
    1.27  \postw
    1.28  
    1.29 -We could continue like this and sketch a complete theory of AA trees without
    1.30 -performing a single proof. Once the definitions and main theorems are in place
    1.31 -and have been thoroughly tested using Nitpick, we could start working on the
    1.32 -proofs. Developing theories this way usually saves time, because faulty theorems
    1.33 -and definitions are discovered much earlier in the process.
    1.34 +We could continue like this and sketch a complete theory of AA trees. Once the
    1.35 +definitions and main theorems are in place and have been thoroughly tested using
    1.36 +Nitpick, we could start working on the proofs. Developing theories this way
    1.37 +usually saves time, because faulty theorems and definitions are discovered much
    1.38 +earlier in the process.
    1.39  
    1.40  \section{Option Reference}
    1.41  \label{option-reference}