# HG changeset patch
# User nipkow
# Date 982403033 -3600
# Node ID 0d94005e374c9def038a19029b64add1be4ae38e
# Parent  1d1d9f60c29b27aae03a64d065434c5e4ebec1c3
*** empty log message ***

diff -r 1d1d9f60c29b -r 0d94005e374c doc-src/TutorialI/Advanced/Partial.thy
--- a/doc-src/TutorialI/Advanced/Partial.thy	Fri Feb 16 18:51:19 2001 +0100
+++ b/doc-src/TutorialI/Advanced/Partial.thy	Sat Feb 17 10:43:53 2001 +0100
@@ -145,7 +145,7 @@
      x := s; while b(x) do x := c(x); return x
 \end{verbatim}
 In general, @{term s} will be a tuple (better still: a record). As an example
-consider the tail recursive variant of function @{term find} above:
+consider the following definition of function @{term find} above:
 *}
 
 constdefs find2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
diff -r 1d1d9f60c29b -r 0d94005e374c doc-src/TutorialI/Advanced/document/Partial.tex
--- a/doc-src/TutorialI/Advanced/document/Partial.tex	Fri Feb 16 18:51:19 2001 +0100
+++ b/doc-src/TutorialI/Advanced/document/Partial.tex	Sat Feb 17 10:43:53 2001 +0100
@@ -154,7 +154,7 @@
      x := s; while b(x) do x := c(x); return x
 \end{verbatim}
 In general, \isa{s} will be a tuple (better still: a record). As an example
-consider the tail recursive variant of function \isa{find} above:%
+consider the following definition of function \isa{find} above:%
 \end{isamarkuptext}%
 \isacommand{constdefs}\ find{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
 \ \ {\isachardoublequote}find{\isadigit{2}}\ f\ x\ {\isasymequiv}\isanewline