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 \ 'a) \ 'a \ 'a"