diff -r ff585297e9f5 -r 25bb0a883ac5 doc-src/TutorialI/Advanced/Partial.thy
--- 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}