--- a/src/Doc/Nitpick/document/root.tex Wed May 21 14:09:43 2014 +0200
+++ b/src/Doc/Nitpick/document/root.tex Wed May 21 14:09:43 2014 +0200
@@ -143,33 +143,33 @@
\section{Installation}
\label{installation}
-Nitpick is part of Isabelle, so you don't need to install it. However, it
-relies on a third-party Kodkod front-end called Kodkodi as well as a Java
-virtual machine called \texttt{java} (version 1.5 or above).
-
-There are two main ways of installing Kodkodi:
-
-\begin{enum}
-\item[\labelitemi] If you installed an official Isabelle package,
-it should already include a properly setup version of Kodkodi.
-
-\item[\labelitemi] If you use a repository or snapshot version of Isabelle, you
-an official Isabelle package, you can download the Isabelle-aware Kodkodi package
-from \url{http://www21.in.tum.de/~blanchet/\#software}. Extract the archive, then add a
-line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash components}%
-\footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at
-startup. Its value can be retrieved by executing \texttt{isabelle}
-\texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.}
-file with the absolute path to Kodkodi. For example, if the
-\texttt{components} file does not exist yet and you extracted Kodkodi to
-\texttt{/usr/local/kodkodi-1.5.2}, create it with the single line
-
-\prew
-\texttt{/usr/local/kodkodi-1.5.2}
-\postw
-
-(including an invisible newline character) in it.
-\end{enum}
+Nitpick is part of Isabelle, so you do not need to install it. It relies on a
+third-party Kodkod front-end called Kodkodi, which in turn requires a Java
+virtual machine. Both are provided as official Isabelle components.
+
+%There are two main ways of installing Kodkodi:
+%
+%\begin{enum}
+%\item[\labelitemi] If you installed an official Isabelle package,
+%it should already include a properly setup version of Kodkodi.
+%
+%\item[\labelitemi] If you use a repository or snapshot version of Isabelle, you
+%an official Isabelle package, you can download the Isabelle-aware Kodkodi package
+%from \url{http://www21.in.tum.de/~blanchet/\#software}. Extract the archive, then add a
+%line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash components}%
+%\footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at
+%startup. Its value can be retrieved by executing \texttt{isabelle}
+%\texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.}
+%file with the absolute path to Kodkodi. For example, if the
+%\texttt{components} file does not exist yet and you extracted Kodkodi to
+%\texttt{/usr/local/kodkodi-1.5.2}, create it with the single line
+%
+%\prew
+%\texttt{/usr/local/kodkodi-1.5.2}
+%\postw
+%
+%(including an invisible newline character) in it.
+%\end{enum}
To check whether Kodkodi is successfully installed, you can try out the example
in \S\ref{propositional-logic}.
--- a/src/Doc/Sledgehammer/document/root.tex Wed May 21 14:09:43 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Wed May 21 14:09:43 2014 +0200
@@ -14,6 +14,9 @@
\newcommand\download{\url{http://isabelle.in.tum.de/components/}}
+\let\oldS=\S
+\def\S{\oldS\,}
+
\def\qty#1{\ensuremath{\left<\mathit{#1\/}\right>}}
\def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1\/}}\right>}$}
@@ -601,8 +604,8 @@
Problems can be easy for \textit{auto} and difficult for automatic provers, but
the reverse is also true, so do not be discouraged if your first attempts fail.
Because the system refers to all theorems known to Isabelle, it is particularly
-suitable when your goal has a short proof from lemmas that you do not know
-about.
+suitable when your goal has a short proof but requires lemmas that you do not
+know about.
\point{Why are there so many options?}
@@ -614,6 +617,7 @@
\label{command-syntax}
\subsection{Sledgehammer}
+\label{sledgehammer}
Sledgehammer can be invoked at any point when there is an open goal by entering
the \textbf{sledgehammer} command in the theory file. Its general syntax is as
@@ -728,6 +732,7 @@
also more concise.
\subsection{Metis}
+\label{metis}
The \textit{metis} proof method has the syntax
@@ -1087,7 +1092,9 @@
\texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or via the ``Mash'' option
under ``Plugins > Plugin Options > Isabelle > General'' in Isabelle/jEdit.
Persistent data for both engines is stored in the directory
-\texttt{\$ISABELLE\_HOME\_USER/mash}.
+\texttt{\$ISABELLE\_HOME\_USER/mash}. When switching to the \textit{py} engine,
+it is recommended to invoke the \textit{relearn\_isar} subcommand
+(\S\ref{sledgehammer}) to synchronize the Python persistent databases.
\item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the
rankings from MePo and MaSh.
@@ -1102,10 +1109,10 @@
takes a value that was empirically found to be appropriate for the prover.
Typical values range between 50 and 1000.
-For the MaSh-related commands \textit{learn\_isar}, \textit{learn\_prover},
-\textit{relearn\_isar}, and \textit{relearn\_prover}, this option specifies the
-maximum number of facts from the background library that should be learned
-($\infty$ by default).
+For the MaSh-related subcommands \textit{learn\_isar}, \textit{learn\_prover},
+\textit{relearn\_isar}, and \textit{relearn\_prover} (\S\ref{sledgehammer}),
+this option specifies the maximum number of facts from the background library
+that should be learned ($\infty$ by default).
\opdefault{fact\_thresholds}{float\_pair}{\upshape 0.45~0.85}
Specifies the thresholds above which facts are considered relevant by the
@@ -1216,7 +1223,7 @@
\item[\labelitemi] \textbf{\textit{poly\_args} (unsound):}
Like for \textit{poly\_guards} constants are annotated with their types to
resolve overloading, but otherwise no type information is encoded. This
-is the default encoding used by the \textit{metis} command.
+is the default encoding used by the \textit{metis} proof method.
\item[\labelitemi]
\textbf{%