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}