author wenzelm Sat, 11 Mar 2006 17:24:37 +0100 changeset 19248 25bb0a883ac5 parent 19247 ff585297e9f5 child 19249 86c73395c99b
renamed const minus to subtract;
--- a/doc-src/TutorialI/Advanced/Partial.thy	Sat Mar 11 16:56:09 2006 +0100
+++ b/doc-src/TutorialI/Advanced/Partial.thy	Sat Mar 11 17:24:37 2006 +0100
@@ -34,8 +34,8 @@
preconditions:
*}

-constdefs minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-"n \<le> m \<Longrightarrow> minus m n \<equiv> m - n"
+constdefs subtract :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+"n \<le> m \<Longrightarrow> subtract m n \<equiv> m - n"

text{*
The rest of this section is devoted to the question of how to define
@@ -49,7 +49,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 @{const minus} above). Instead we have to move the condition over
+(see @{const 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}
--- 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}