# HG changeset patch
# User blanchet
# Date 1277298400 -7200
# Node ID 19ba7ec5f1e32b145e8bb3e3d94ff1295dd32774
# Parent  c81c86bfc18add9194a989792b3e62ff4aca2ca9
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs

diff -r c81c86bfc18a -r 19ba7ec5f1e3 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Wed Jun 23 14:36:23 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed Jun 23 15:06:40 2010 +0200
@@ -83,14 +83,19 @@
 can be run locally or remotely via the SystemOnTPTP web service
 \cite{sutcliffe-2000}.
 
-The problem passed to ATPs consists of the current goal together with a
-heuristic selection of facts (theorems) from the current theory context,
-filtered by relevance. The result of a successful ATP proof search is some
-source text that usually (but not always) reconstructs the proof within
-Isabelle, without requiring the ATPs again. The reconstructed proof relies on
-the general-purpose Metis prover \cite{metis}, which is fully integrated into
-Isabelle/HOL, with explicit inferences going through the kernel. Thus its
-results are correct by construction.
+The problem passed to ATPs consists of your current goal together with a
+heuristic selection of hundreds of facts (theorems) from the current theory
+context, filtered by relevance. Because jobs are run in the background, you can
+continue to work on your proof by other means. Provers can be run in parallel.
+Any reply (which may arrive minutes later) will appear in the Proof General
+response buffer.
+
+The result of a successful ATP proof search is some source text that usually
+(but not always) reconstructs the proof within Isabelle, without requiring the
+ATPs again. The reconstructed proof relies on the general-purpose Metis prover
+\cite{metis}, which is fully integrated into Isabelle/HOL, with explicit
+inferences going through the kernel. Thus its results are correct by
+construction.
 
 \newbox\boxA
 \setbox\boxA=\hbox{\texttt{nospam}}
@@ -143,6 +148,9 @@
 To check whether E and SPASS are installed, follow the example in
 \S\ref{first-steps}.
 
+Remote ATP invocation via the SystemOnTPTP web service requires Perl with the
+World Wide Web Library (\texttt{libwww-perl}) installed.
+
 \section{First Steps}
 \label{first-steps}
 
@@ -158,7 +166,10 @@
 \textbf{sledgehammer}
 \postw
 
-After a few seconds, Sledgehammer produces the following output:
+Instead of issuing the \textbf{sledgehammer} command, you can also find
+Sledgehammer in the ``Commands'' submenu of the ``Isabelle'' menu in Proof
+General or press the Emacs key sequence C-c C-a C-s.
+Either way, Sledgehammer produces the following output after a few seconds:
 
 \prew
 \slshape
@@ -206,6 +217,23 @@
 readable and also faster than the \textit{metis} one-liners. This feature is
 experimental.
 
+\section{Hints}
+\label{hints}
+
+For best results, first simplify your problem by calling \textit{auto} or at
+least \textit{safe} followed by \textit{simp\_all}. None of the ATPs contain
+arithmetic decision procedures. They are not especially good at heavy rewriting,
+but because they regard equations as undirected, they often prove theorems that
+require the reverse orientation of a \textit{simp} rule. Higher-order problems
+can be tackled, but the success rate is better for first-order problems. Hence,
+you may get better results if you first simplify the problem to remove
+higher-order features.
+
+Note that problems can be easy for auto and difficult for ATPs, but the reverse
+is also true, so don't 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 don't know about.
+
 \section{Command Syntax}
 \label{command-syntax}