--- a/doc-src/TutorialI/Misc/document/simp.tex Wed Jun 22 07:54:13 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/simp.tex Wed Jun 22 09:26:18 2005 +0200
@@ -441,7 +441,7 @@
\begin{isamarkuptext}%
\indexbold{tracing the simplifier}
Using the simplifier effectively may take a bit of experimentation. Set the
-Proof General flag \textsf{Isabelle} $>$ \textsf{Settings} $>$ \textsf{Trace Simplifier} to get a better idea of what is going on:%
+Proof General flag \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ \pgmenu{Trace Simplifier} to get a better idea of what is going on:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ {\isachardoublequote}rev\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
@@ -451,7 +451,7 @@
%
\begin{isamarkuptext}%
\noindent
-produces the following trace in Proof General's \textsf{Trace} buffer:
+produces the following trace in Proof General's \pgmenu{Trace} buffer:
\begin{ttbox}\makeatother
[1]Applying instance of rewrite rule "List.rev.simps_2":
@@ -491,7 +491,7 @@
Many other hints about the simplifier's actions may appear.
In more complicated cases, the trace can be very lengthy. Thus it is
-advisable to reset the \textsf{Trace Simplifier} flag after having
+advisable to reset the \pgmenu{Trace Simplifier} flag after having
obtained the desired trace.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -501,12 +501,13 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
+\indexbold{finding theorems}\indexbold{searching theorems}
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.
+The search engine is started by clicking on Proof General's \pgmenu{Find} icon.
You specify your search textually in the input buffer at the bottom
of the window.
\end{pgnote}
@@ -543,13 +544,14 @@
\begin{ttbox}
simp: "_ * (_ + _)"
\end{ttbox}
-This searches all (possibly conditional) equations of the form
+This searches \emph{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.
+not just those with a \isa{simp} attribute.
Note that the given pattern needs to be simplified
-at the root, not somewhere inside.
+at the root, not somewhere inside: for example, commutativity of \isa{{\isacharplus}}
+does not match.
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
@@ -561,9 +563,10 @@
Search criteria can also be negated by prefixing them with ``\texttt{-}'':
\begin{ttbox}
--name: HOL
+-name: List
\end{ttbox}
-finds theorems whose name does not contain \texttt{HOL}. This is useful for
+finds theorems whose name does not contain \texttt{List}. This can be useful,
+for example, for
excluding particular theories from the search because the (long) name of
a theorem contains the name of the theory it comes from.
@@ -571,10 +574,17 @@
\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}.
+looks for theorems containg a plus but no minus which do not simplify
+\mbox{\isa{{\isacharunderscore}\ {\isacharasterisk}\ {\isacharparenleft}{\isacharunderscore}\ {\isacharplus}\ {\isacharunderscore}{\isacharparenright}}} at the root and whose name contains \texttt{assoc}.
+
+Further search criteria are explained in \S\ref{sec:find:ied}.
-Further search criteria are explained in \S\ref{sec:Find:ied}.%
+\begin{pgnote}
+Proof General keeps a history of all your search expressions.
+If you click on \pgmenu{Find}, you can use the arrow keys to scroll
+through previous searches and just modify them. This saves you having
+to type in lengthy expressions again and again.
+\end{pgnote}%
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%