1.1 --- a/src/Doc/Nitpick/document/root.tex	Fri Sep 20 22:39:30 2013 +0200
     1.2 +++ b/src/Doc/Nitpick/document/root.tex	Fri Sep 20 22:39:30 2013 +0200
     1.3 @@ -114,16 +114,9 @@
     1.4  must find a model for the axioms. If it finds no model, we have an indication
     1.5  that the axioms might be unsatisfiable.
     1.6  
     1.7 -You can also invoke Nitpick from the ``Commands'' submenu of the
     1.8 -``Isabelle'' menu in Proof General or by pressing the Emacs key sequence C-c C-a
     1.9 -C-n. This is equivalent to entering the \textbf{nitpick} command with no
    1.10 -arguments in the theory text.
    1.11 -
    1.12 -Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
    1.13 -Nitpick also provides an automatic mode that can be enabled via the ``Auto
    1.14 -Nitpick'' option from the ``Isabelle'' menu in Proof General. In this mode,
    1.15 -Nitpick is run on every newly entered theorem. The time limit for Auto Nitpick
    1.16 -and other automatic tools can be set using the ``Auto Tools Time Limit'' option.
    1.17 +For Isabelle/jEdit users, Nitpick provides an automatic mode that can be enabled
    1.18 +via the ``Auto Nitpick'' option under ``Plugins > Plugin Options > Isabelle >
    1.19 +General.'' In this mode, Nitpick is run on every newly entered theorem.
    1.20  
    1.21  \newbox\boxA
    1.22  \setbox\boxA=\hbox{\texttt{nospam}}
    1.23 @@ -148,7 +141,7 @@
    1.24  \section{Installation}
    1.25  \label{installation}
    1.26  
    1.27 -Sledgehammer is part of Isabelle, so you don't need to install it. However, it
    1.28 +Nitpick is part of Isabelle, so you don't need to install it. However, it
    1.29  relies on a third-party Kodkod front-end called Kodkodi as well as a Java
    1.30  virtual machine called \texttt{java} (version 1.5 or above).
    1.31  
    1.32 @@ -1874,17 +1867,18 @@
    1.33  (\S\ref{authentication}), optimizations
    1.34  (\S\ref{optimizations}), and timeouts (\S\ref{timeouts}).
    1.35  
    1.36 -You can instruct Nitpick to run automatically on newly entered theorems by
    1.37 -enabling the ``Auto Nitpick'' option from the ``Isabelle'' menu in Proof
    1.38 -General. For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation}),
    1.39 +If you use Isabelle/jEdit, Nitpick also provides an automatic mode that can
    1.40 +be enabled via the ``Auto Nitpick'' option under ``Plugins > Plugin Options
    1.41 +> Isabelle > General.'' For automatic runs,
    1.42 +\textit{user\_axioms} (\S\ref{mode-of-operation}),
    1.43  \textit{assms} (\S\ref{mode-of-operation}), and \textit{mono}
    1.44  (\S\ref{scope-of-search}) are implicitly enabled, \textit{blocking}
    1.45  (\S\ref{mode-of-operation}), \textit{verbose} (\S\ref{output-format}), and
    1.46  \textit{debug} (\S\ref{output-format}) are disabled, \textit{max\_threads}
    1.47  (\S\ref{optimizations}) is taken to be 1, \textit{max\_potential}
    1.48  (\S\ref{output-format}) is taken to be 0, and \textit{timeout}
    1.49 -(\S\ref{timeouts}) is superseded by the ``Auto Tools Time Limit'' in
    1.50 -Proof General's ``Isabelle'' menu. Nitpick's output is also more concise.
    1.51 +(\S\ref{timeouts}) is superseded by the ``Auto Time Limit'' in jEdit. Nitpick's
    1.52 +output is also more concise.
    1.53  
    1.54  The number of options can be overwhelming at first glance. Do not let that worry
    1.55  you: Nitpick's defaults have been chosen so that it almost always does the right
    1.56 @@ -2523,10 +2517,9 @@
    1.57  \opdefault{timeout}{float\_or\_none}{\upshape 30}
    1.58  Specifies the maximum number of seconds that the \textbf{nitpick} command should
    1.59  spend looking for a counterexample. Nitpick tries to honor this constraint as
    1.60 -well as it can but offers no guarantees. For automatic runs,
    1.61 -\textit{timeout} is ignored; instead, Auto Quickcheck and Auto Nitpick share
    1.62 -a time slot whose length is specified by the ``Auto Counterexample Time
    1.63 -Limit'' option in Proof General.
    1.64 +well as it can but offers no guarantees. For automatic runs, the ``Auto Time
    1.65 +Limit'' option under ``Plugins > Plugin Options > Isabelle > General'' is used
    1.66 +instead.
    1.67  
    1.68  \nopagebreak
    1.69  {\small See also \textit{max\_threads} (\S\ref{optimizations}).}

     2.1 --- a/src/Doc/Sledgehammer/document/root.tex	Fri Sep 20 22:39:30 2013 +0200
     2.2 +++ b/src/Doc/Sledgehammer/document/root.tex	Fri Sep 20 22:39:30 2013 +0200
     2.3 @@ -112,11 +112,6 @@
     2.4  The problem passed to the automatic provers consists of your current goal
     2.5  together with a heuristic selection of hundreds of facts (theorems) from the
     2.6  current theory context, filtered by relevance.
     2.7 -%Because jobs are run in the
     2.8 -%background, you can continue to work on your proof by other means. Provers can
     2.9 -%be run in parallel.
    2.10 -%Any reply (which may arrive half a minute later) will appear
    2.11 -%in the Proof General response buffer.
    2.12  
    2.13  The result of a successful proof search is some source text that usually (but
    2.14  not always) reconstructs the proof within Isabelle. For ATPs, the reconstructed
    2.15 @@ -124,12 +119,10 @@
    2.16  integrates the Metis ATP in Isabelle/HOL with explicit inferences going through
    2.17  the kernel. Thus its results are correct by construction.
    2.18  
    2.19 -In this manual, we will explicitly invoke the \textbf{sledgehammer} command.
    2.20 -For Proof General users, Sledgehammer also provides an automatic mode that can
    2.21 -be enabled via the ``Auto Sledgehammer'' option in the ``Isabelle'' menu. In
    2.22 -this mode, Sledgehammer is run on every newly entered theorem. The time limit
    2.23 -for Auto Sledgehammer and other automatic tools can be set using the ``Auto
    2.24 -Tools Time Limit'' option.
    2.25 +For Isabelle/jEdit users, Sledgehammer provides an automatic mode that can be
    2.26 +enabled via the ``Auto Sledgehammer'' option under ``Plugins > Plugin Options >
    2.27 +Isabelle > General.'' In this mode, Sledgehammer is run on every newly entered
    2.28 +theorem.
    2.29  
    2.30  \newbox\boxA
    2.31  \setbox\boxA=\hbox{\texttt{NOSPAM}}
    2.32 @@ -268,11 +261,9 @@
    2.33  \textbf{sledgehammer}
    2.34  \postw
    2.35  
    2.36 -%Instead of issuing the \textbf{sledgehammer} command, you can also find
    2.37 -%Sledgehammer in the ``Commands'' submenu of the ``Isabelle'' menu in Proof
    2.38 -%General or press the Emacs key sequence C-c C-a C-s.
    2.39 -%Either way,
    2.40 -Sledgehammer produces the following output after a few seconds:
    2.41 +Instead of issuing the \textbf{sledgehammer} command, you can also use the
    2.42 +Sledgehammer panel in Isabelle/jEdit. Sledgehammer produces the following output
    2.43 +after a few seconds:
    2.44  
    2.45  \prew
    2.46  \slshape
    2.47 @@ -345,7 +336,7 @@
    2.48  Locally installed provers are faster and more reliable than those running on
    2.49  servers. See \S\ref{installation} for details on how to install them.
    2.50  
    2.51 -\point{Familiarize yourself with the most important options}
    2.52 +\point{Familiarize yourself with the main options}
    2.53  
    2.54  Sledgehammer's options are fully documented in \S\ref{command-syntax}. Many of
    2.55  the options are very specialized, but serious users of the tool should at least
    2.56 @@ -411,7 +402,7 @@
    2.57  and it cannot learn.
    2.58  
    2.59  \item[\labelitemi]
    2.60 -An experimental, memoryful alternative to MePo is \emph{MaSh}
    2.61 +An experimental alternative to MePo is \emph{MaSh}
    2.62  (\underline{Ma}chine Learner for \underline{S}ledge\underline{h}ammer). It
    2.63  relies on an external Python tool that applies machine learning to
    2.64  the problem of finding relevant facts.
    2.65 @@ -529,7 +520,7 @@
    2.66  
    2.67  The \textit{metis}~(\textit{full\_types}) proof method
    2.68  and its cousin \textit{metis}~(\textit{mono\_tags}) are fully-typed
    2.69 -version of Metis. It is somewhat slower than \textit{metis}, but the proof
    2.70 +versions of Metis. It is somewhat slower than \textit{metis}, but the proof
    2.71  search is fully typed, and it also includes more powerful rules such as the
    2.72  axiom ``$x = \const{True} \mathrel{\lor} x = \const{False}$'' for reasoning in
    2.73  higher-order places (e.g., in set comprehensions). The method kicks in
    2.74 @@ -635,12 +626,6 @@
    2.75  \textbf{sledgehammer} \qty{subcommand}$^?$ \qty{options}$^?$ \qty{facts\_override}$^?$ \qty{num}$^?$
    2.76  \postw
    2.77  
    2.78 -For Proof General users,
    2.79 -Sledgehammer is also available in the ``Commands'' submenu of
    2.80 -the ``Isabelle'' menu or by pressing the Emacs key sequence C-c
    2.81 -C-a C-s. This is equivalent to entering the \textbf{sledgehammer} command with
    2.82 -no arguments in the theory text.
    2.83 -
    2.84  In the general syntax, the \qty{subcommand} may be any of the following:
    2.85  
    2.86  \begin{enum}
    2.87 @@ -731,16 +716,15 @@
    2.88  proceed as usual except that it should consider \qty{facts\/_{\mathrm{1}}}
    2.89  highly-relevant and \qty{facts\/_{\mathrm{2}}} fully irrelevant.
    2.90  
    2.91 -If you use Proof General, you can instruct Sledgehammer to run automatically on
    2.92 -newly entered theorems by enabling the ``Auto Sledgehammer'' option in the
    2.93 -``Isabelle'' menu. For automatic runs, only the first prover set using
    2.94 +If you use Isabelle/jEdit, Sledgehammer also provides an automatic mode that can
    2.95 +be enabled via the ``Auto Sledgehammer'' option under ``Plugins > Plugin Options
    2.96 +> Isabelle > General.'' For automatic runs, only the first prover set using
    2.97  \textit{provers} (\S\ref{mode-of-operation}) is considered, fewer facts are
    2.98  passed to the prover, \textit{slice} (\S\ref{mode-of-operation}) is disabled,
    2.99  \textit{strict} (\S\ref{problem-encoding}) is enabled, \textit{verbose}
   2.100  (\S\ref{output-format}) and \textit{debug} (\S\ref{output-format}) are disabled,
   2.101 -and \textit{timeout} (\S\ref{timeouts}) is superseded by the ``Auto Tools Time
   2.102 -Limit'' in the ``Isabelle'' menu. Sledgehammer's output is also more
   2.103 -concise.
   2.104 +and \textit{timeout} (\S\ref{timeouts}) is superseded by the ``Auto Time Limit''
   2.105 +option in jEdit. Sledgehammer's output is also more concise.
   2.106  
   2.107  \subsection{Metis}
   2.108  
   2.109 @@ -986,9 +970,7 @@
   2.110  
   2.111  By default, Sledgehammer runs a selection of CVC3, E, E-SInE, SPASS, Vampire,
   2.112  Yices, and Z3 in parallel---either locally or remotely, depending on the number
   2.113 -of processor cores available. (For historical reasons, the default value of this
   2.114 -option can be overridden using the option ``Sledgehammer: Provers'' in Proof
   2.115 -General's ``Isabelle'' menu.)
   2.116 +of processor cores available.
   2.117  
   2.118  It is generally a good idea to run several provers in parallel. Running E,
   2.119  SPASS, and Vampire for 5~seconds yields a similar success rate to running the
   2.120 @@ -1005,8 +987,8 @@
   2.121  synchronously. The asynchronous (non-blocking) mode lets the user start proving
   2.122  the putative theorem manually while Sledgehammer looks for a proof, but it can
   2.123  also be more confusing. Irrespective of the value of this option, Sledgehammer
   2.124 -is always run synchronously for the new jEdit-based user interface or if
   2.125 -\textit{debug} (\S\ref{output-format}) is enabled.
   2.126 +is always run synchronously if \textit{debug} (\S\ref{output-format}) is
   2.127 +enabled.
   2.128  
   2.129  \optrue{slice}{dont\_slice}
   2.130  Specifies whether the time allocated to a prover should be sliced into several
   2.131 @@ -1057,10 +1039,10 @@
   2.132  The traditional memoryless MePo relevance filter.
   2.133  
   2.134  \item[\labelitemi] \textbf{\textit{mash}:}
   2.135 -The experimental, memoryful MaSh machine learner. MaSh relies on the external
   2.136 -Python program \texttt{mash.py}, which is part of Isabelle. To enable MaSh, set
   2.137 -the environment variable \texttt{MASH} to \texttt{yes}. Persistent data is
   2.138 -stored in the directory \texttt{\$ISABELLE\_HOME\_USER/mash}.
   2.139 +The experimental MaSh machine learner. MaSh relies on the external Python
   2.140 +program \texttt{mash.py}, which is part of Isabelle. To enable MaSh, set the
   2.141 +environment variable \texttt{MASH} to \texttt{yes}. Persistent data is stored in
   2.142 +the directory \texttt{\$ISABELLE\_HOME\_USER/mash}.
   2.143  
   2.144  \item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the
   2.145  rankings from MePo and MaSh.
   2.146 @@ -1090,8 +1072,8 @@
   2.147  
   2.148  \optrue{learn}{dont\_learn}
   2.149  Specifies whether MaSh should be run automatically by Sledgehammer to learn the
   2.150 -available theories (and hence provide more accurate results). Learning only
   2.151 -takes place if MaSh is enabled.
   2.152 +available theories (and hence provide more accurate results). Learning takes
   2.153 +place only if MaSh is enabled.
   2.154  
   2.155  \opdefault{max\_new\_mono\_instances}{int}{smart}
   2.156  Specifies the maximum number of monomorphic instances to generate beyond
   2.157 @@ -1349,8 +1331,8 @@
   2.158  \opdefault{timeout}{float\_or\_none}{\upshape 30}
   2.159  Specifies the maximum number of seconds that the automatic provers should spend
   2.160  searching for a proof. This excludes problem preparation and is a soft limit.
   2.161 -(For historical reasons, the default value of this option can be overridden using
   2.162 -the option ``Sledgehammer: Time Limit'' in Proof General's ``Isabelle'' menu.)
   2.163 +For automatic runs, the ``Auto Time Limit'' option under ``Plugins > Plugin
   2.164 +Options > Isabelle > General'' is used instead.
   2.165  
   2.166  \opdefault{preplay\_timeout}{float\_or\_none}{\upshape 3}
   2.167  Specifies the maximum number of seconds that \textit{metis} or \textit{smt}