# HG changeset patch
# User nipkow
# Date 1119462228 -7200
# Node ID 29828ddbf6ee7bf3a51b870dc426b00595e3632f
# Parent  4dd8b4d1cfc322e790d19a49a321c35a59482f58
tunes Find

diff -r 4dd8b4d1cfc3 -r 29828ddbf6ee doc-src/TutorialI/Misc/simp.thy
--- a/doc-src/TutorialI/Misc/simp.thy	Wed Jun 22 19:43:38 2005 +0200
+++ b/doc-src/TutorialI/Misc/simp.thy	Wed Jun 22 19:43:48 2005 +0200
@@ -418,7 +418,7 @@
 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
@@ -494,7 +494,7 @@
 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.