# HG changeset patch
# User nipkow
# Date 1119462243 -7200
# Node ID 916aa587dfbd2498b04691ee86221481b3258f4c
# Parent  29828ddbf6ee7bf3a51b870dc426b00595e3632f
*** empty log message ***

diff -r 29828ddbf6ee -r 916aa587dfbd doc-src/TutorialI/Misc/document/simp.tex
--- a/doc-src/TutorialI/Misc/document/simp.tex	Wed Jun 22 19:43:48 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Wed Jun 22 19:44:03 2005 +0200
@@ -496,7 +496,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Finding Theorems%
+\isamarkupsubsection{Finding Theorems\label{sec:find}%
 }
 \isamarkuptrue%
 %
@@ -577,7 +577,7 @@
 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:find2}.
 
 \begin{pgnote}
 Proof General keeps a history of all your search expressions.