diff -r 086c6a97f340 -r b3235bd87da7 doc-src/TutorialI/Misc/document/simp.tex
--- a/doc-src/TutorialI/Misc/document/simp.tex	Tue Jun 21 21:38:27 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Tue Jun 21 21:41:08 2005 +0200
@@ -454,34 +454,34 @@
 produces the following trace in Proof General's \textsf{Trace} buffer:
 
 \begin{ttbox}\makeatother
-[0]Applying instance of rewrite rule "List.rev.simps_2":
+[1]Applying instance of rewrite rule "List.rev.simps_2":
 rev (?x1 # ?xs1) \(\equiv\) rev ?xs1 @ [?x1]
 
-[0]Rewriting:
+[1]Rewriting:
 rev [a] \(\equiv\) rev [] @ [a]
 
-[0]Applying instance of rewrite rule "List.rev.simps_1":
+[1]Applying instance of rewrite rule "List.rev.simps_1":
 rev [] \(\equiv\) []
 
-[0]Rewriting:
+[1]Rewriting:
 rev [] \(\equiv\) []
 
-[0]Applying instance of rewrite rule "List.op @.append_Nil":
+[1]Applying instance of rewrite rule "List.op @.append_Nil":
 [] @ ?y \(\equiv\) ?y
 
-[0]Rewriting:
+[1]Rewriting:
 [] @ [a] \(\equiv\) [a]
 
-[0]Applying instance of rewrite rule
+[1]Applying instance of rewrite rule
 ?x2 # ?t1 = ?t1 \(\equiv\) False
 
-[0]Rewriting:
+[1]Rewriting:
 [a] = [] \(\equiv\) False
 \end{ttbox}
 The trace lists each rule being applied, both in its general form and
 the instance being used. The \texttt{[}$i$\texttt{]} in front (where
-above $i$ is always \texttt{0}) indicates that we are inside the $i$th
-recursive invocation of the simplifier. Each attempt to apply a
+above $i$ is always \texttt{1}) indicates that we are inside the $i$th
+invocation of the simplifier. Each attempt to apply a
 conditional rule shows the rule followed by the trace of the
 (recursive!) simplification of the conditions, the latter prefixed by
 \texttt{[}$i+1$\texttt{]} instead of \texttt{[}$i$\texttt{]}.
@@ -495,6 +495,88 @@
 obtained the desired trace.%
 \end{isamarkuptext}%
 \isamarkuptrue%
+%
+\isamarkupsubsection{Finding Theorems%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isabelle's large database of already proved theorems requires
+and offers a powerful yet simple search engine. Its only limitation is
+its restriction to the theories currently loaded.
+
+\begin{pgnote}
+The search engine is started by clicking on Proof General's \textsf{Find} icon.
+You specify your search textually in the input buffer at the bottom
+of the window.
+\end{pgnote}
+
+The simplest form of search is that for theorems containing particular
+patterns: just type in the pattern(s). A pattern can be any term (even
+a single identifier) and may contain ``\texttt{\_}''. Here are some
+examples:
+\begin{ttbox}
+length
+"_ # _ = _ # _"
+"_ + _"
+"_ * (_ - (_::nat))"
+\end{ttbox}
+Note the ability to specify types to narrow searches involving overloaded
+operators.
+
+If you specify more than one pattern, all of them must be present in a
+theorem to match.
+
+\begin{warn}
+Always use ``\texttt{\_}'' rather than variable names: searching for
+\texttt{"x + y"} will usually not find any matching theorems
+because they would need to contain literally \texttt{x} and \texttt{y}.
+This is a feature, not a  bug.
+
+When searching for infix operators, do not just type in the symbol:
+\texttt{+} is not a proper term, you  need to say \texttt{"_ + _"}.
+This applies to other, more complicated syntaxes, too.
+\end{warn}
+
+If you are looking for theorems potentially simplifying some term, you
+need to prefix the pattern with \texttt{simp:}.
+\begin{ttbox}
+simp: "_ * (_ + _)"
+\end{ttbox}
+This searches all (possibly conditional) equations of the form
+\begin{isabelle}%
+\ \ \ \ \ {\isacharunderscore}\ {\isacharasterisk}\ {\isacharparenleft}{\isacharunderscore}\ {\isacharplus}\ {\isacharunderscore}{\isacharparenright}\ {\isacharequal}\ {\isasymdots}%
+\end{isabelle}
+i.e.\ all distributivity rules.
+Note that the given pattern needs to be simplified
+at the root, not somewhere inside.
+
+You may also search theorems by name. To make this useful you merely
+need to give a substring. For example, you could try and search for all
+commutativity theorems like this:
+\begin{ttbox}
+name: comm
+\end{ttbox}
+This retrieves all theorems whose name contains \texttt{comm}.
+
+Search criteria can also be negated by prefixing them with ``\texttt{-}'':
+\begin{ttbox}
+-name: HOL
+\end{ttbox}
+finds theorems whose name does not contain \texttt{HOL}. This is useful for
+excluding particular theories from the search because the (long) name of
+a theorem contains the name of the theory it comes from.
+
+Finallly, different search criteria can be combined arbitrarily:
+\begin{ttbox}
+"_ + _"  -"_ - _"  -simp: "_ * (_ + _)"  name: assoc
+\end{ttbox}
+looks for theorems containg a plus but no minus which are not distributivity
+rules and whose name contains \texttt{assoc}.
+
+Further search criteria are explained in \S\ref{sec:Find:ied}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
 \isamarkupfalse%
 \end{isabellebody}%
 %%% Local Variables: