*** empty log message ***
authornipkow
Wed, 22 Jun 2005 19:44:03 +0200
changeset 16545 916aa587dfbd
parent 16544 29828ddbf6ee
child 16546 77e7fd18b785
*** empty log message ***
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.