# HG changeset patch
# User wenzelm
# Date 1142094277 -3600
# Node ID 25bb0a883ac58a6473cb82eca61cd72896edb91a
# Parent  ff585297e9f50d3cc81fc80ce05d0c91bd5f1e53
renamed const minus to subtract;

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