doc-src/TutorialI/fp.tex
changeset 11215 b44ad7e4c4d2
parent 11214 3b3cc0cf533f
child 11294 16481a4cc9f3
--- a/doc-src/TutorialI/fp.tex	Mon Mar 19 13:05:56 2001 +0100
+++ b/doc-src/TutorialI/fp.tex	Mon Mar 19 13:28:06 2001 +0100
@@ -263,7 +263,7 @@
 
 Note that pattern-matching is not allowed, i.e.\ each definition must be of
 the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.
-Section~{\S}\ref{sec:Simplification} explains how definitions are used
+Section~{\S}\ref{sec:Simp-with-Defs} explains how definitions are used
 in proofs.
 
 \input{Misc/document/prime_def.tex}