# 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.