--- a/doc-src/TutorialI/Advanced/document/Partial.tex Sat Mar 11 16:56:09 2006 +0100
+++ b/doc-src/TutorialI/Advanced/document/Partial.tex Sat Mar 11 17:24:37 2006 +0100
@@ -53,8 +53,8 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{constdefs}\isamarkupfalse%
-\ minus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}n\ {\isasymle}\ m\ {\isasymLongrightarrow}\ minus\ m\ n\ {\isasymequiv}\ m\ {\isacharminus}\ n{\isachardoublequoteclose}%
+\ subtract\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
+{\isachardoublequoteopen}n\ {\isasymle}\ m\ {\isasymLongrightarrow}\ subtract\ m\ n\ {\isasymequiv}\ m\ {\isacharminus}\ n{\isachardoublequoteclose}%
\begin{isamarkuptext}%
The rest of this section is devoted to the question of how to define
partial recursive functions by other means than non-exhaustive pattern
@@ -70,7 +70,7 @@
\index{recursion!guarded}%
Neither \isacommand{primrec} nor \isacommand{recdef} allow to
prefix an equation with a condition in the way ordinary definitions do
-(see \isa{minus} above). Instead we have to move the condition over
+(see \isa{subtract} above). Instead we have to move the condition over
to the right-hand side of the equation. Given a partial function $f$
that should satisfy the recursion equation $f(x) = t$ over its domain
$dom(f)$, we turn this into the \isacommand{recdef}