doc-src/TutorialI/Misc/simp.thy

 
 In more complicated cases, the trace can be very lengthy.  Thus it is
 advisable to reset the \pgmenu{Trace Simplifier} flag after having
 obtained the desired trace.  *}
 
-subsection{*Finding Theorems*}
+subsection{*Finding Theorems\label{sec:find}*}
 
 text{*\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.

 "_ + _"  -"_ - _"  -simp: "_ * (_ + _)"  name: assoc
 \end{ttbox}
 looks for theorems containg a plus but no minus which do not simplify
 \mbox{@{text"_ * (_ + _)"}} 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:find2}.
 
 \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