diff -r 1b2d4f995b13 -r f789d2490669 doc-src/TutorialI/Recdef/document/examples.tex
--- a/doc-src/TutorialI/Recdef/document/examples.tex	Mon Aug 21 19:17:07 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/examples.tex	Mon Aug 21 19:29:27 2000 +0200
@@ -3,30 +3,30 @@
 \begin{isamarkuptext}%
 Here is a simple example, the Fibonacci function:%
 \end{isamarkuptext}%
-\isacommand{consts}\ fib\ ::\ {"}nat\ {\isasymRightarrow}\ nat{"}\isanewline
-\isacommand{recdef}\ fib\ {"}measure({\isasymlambda}n.\ n){"}\isanewline
-\ \ {"}fib\ 0\ =\ 0{"}\isanewline
-\ \ {"}fib\ 1\ =\ 1{"}\isanewline
-\ \ {"}fib\ (Suc(Suc\ x))\ =\ fib\ x\ +\ fib\ (Suc\ x){"}%
+\isacommand{consts}\ fib\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
+\isacommand{recdef}\ fib\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}fib\ \isadigit{0}\ {\isacharequal}\ \isadigit{0}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}fib\ \isadigit{1}\ {\isacharequal}\ \isadigit{1}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}fib\ {\isacharparenleft}Suc{\isacharparenleft}Suc\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ x\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ x{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 The definition of \isa{fib} is accompanied by a \bfindex{measure function}
-\isa{{\isasymlambda}\mbox{n}.\ \mbox{n}} which maps the argument of \isa{fib} to a
+\isa{{\isasymlambda}\mbox{n}{\isachardot}\ \mbox{n}} which maps the argument of \isa{fib} to a
 natural number. The requirement is that in each equation the measure of the
 argument on the left-hand side is strictly greater than the measure of the
 argument of each recursive call. In the case of \isa{fib} this is
 obviously true because the measure function is the identity and
-\isa{Suc\ (Suc\ \mbox{x})} is strictly greater than both \isa{x} and
+\isa{Suc\ {\isacharparenleft}Suc\ \mbox{x}{\isacharparenright}} is strictly greater than both \isa{x} and
 \isa{Suc\ \mbox{x}}.
 
 Slightly more interesting is the insertion of a fixed element
 between any two elements of a list:%
 \end{isamarkuptext}%
-\isacommand{consts}\ sep\ ::\ {"}'a\ *\ 'a\ list\ {\isasymRightarrow}\ 'a\ list{"}\isanewline
-\isacommand{recdef}\ sep\ {"}measure\ ({\isasymlambda}(a,xs).\ length\ xs){"}\isanewline
-\ \ {"}sep(a,\ [])\ \ \ \ \ =\ []{"}\isanewline
-\ \ {"}sep(a,\ [x])\ \ \ \ =\ [x]{"}\isanewline
-\ \ {"}sep(a,\ x\#y\#zs)\ =\ x\ \#\ a\ \#\ sep(a,y\#zs){"}%
+\isacommand{consts}\ sep\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
+\isacommand{recdef}\ sep\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}a{\isacharcomma}xs{\isacharparenright}{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}sep{\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}sep{\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\ \ \ \ {\isacharequal}\ {\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}sep{\isacharparenleft}a{\isacharcomma}\ x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep{\isacharparenleft}a{\isacharcomma}y{\isacharhash}zs{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 This time the measure is the length of the list, which decreases with the
@@ -34,18 +34,18 @@
 
 Pattern matching need not be exhaustive:%
 \end{isamarkuptext}%
-\isacommand{consts}\ last\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a{"}\isanewline
-\isacommand{recdef}\ last\ {"}measure\ ({\isasymlambda}xs.\ length\ xs){"}\isanewline
-\ \ {"}last\ [x]\ \ \ \ \ \ =\ x{"}\isanewline
-\ \ {"}last\ (x\#y\#zs)\ =\ last\ (y\#zs){"}%
+\isacommand{consts}\ last\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
+\isacommand{recdef}\ last\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}xs{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}last\ {\isacharbrackleft}x{\isacharbrackright}\ \ \ \ \ \ {\isacharequal}\ x{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}last\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ last\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 Overlapping patterns are disambiguated by taking the order of equations into
 account, just as in functional programming:%
 \end{isamarkuptext}%
-\isacommand{consts}\ sep1\ ::\ {"}'a\ *\ 'a\ list\ {\isasymRightarrow}\ 'a\ list{"}\isanewline
-\isacommand{recdef}\ sep1\ {"}measure\ ({\isasymlambda}(a,xs).\ length\ xs){"}\isanewline
-\ \ {"}sep1(a,\ x\#y\#zs)\ =\ x\ \#\ a\ \#\ sep1(a,y\#zs){"}\isanewline
-\ \ {"}sep1(a,\ xs)\ \ \ \ \ =\ xs{"}%
+\isacommand{consts}\ sep\isadigit{1}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
+\isacommand{recdef}\ sep\isadigit{1}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}a{\isacharcomma}xs{\isacharparenright}{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}sep\isadigit{1}{\isacharparenleft}a{\isacharcomma}\ x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep\isadigit{1}{\isacharparenleft}a{\isacharcomma}y{\isacharhash}zs{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}sep\isadigit{1}{\isacharparenleft}a{\isacharcomma}\ xs{\isacharparenright}\ \ \ \ \ {\isacharequal}\ xs{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 This defines exactly the same function as \isa{sep} above, i.e.\
@@ -60,18 +60,18 @@
   arguments as in the following definition:
 \end{warn}%
 \end{isamarkuptext}%
-\isacommand{consts}\ sep2\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a\ {\isasymRightarrow}\ 'a\ list{"}\isanewline
-\isacommand{recdef}\ sep2\ {"}measure\ length{"}\isanewline
-\ \ {"}sep2\ (x\#y\#zs)\ =\ ({\isasymlambda}a.\ x\ \#\ a\ \#\ sep2\ zs\ a){"}\isanewline
-\ \ {"}sep2\ xs\ \ \ \ \ \ \ =\ ({\isasymlambda}a.\ xs){"}%
+\isacommand{consts}\ sep\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
+\isacommand{recdef}\ sep\isadigit{2}\ {\isachardoublequote}measure\ length{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}sep\isadigit{2}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep\isadigit{2}\ zs\ a{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}sep\isadigit{2}\ xs\ \ \ \ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ xs{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 Because of its pattern-matching syntax, \isacommand{recdef} is also useful
 for the definition of non-recursive functions:%
 \end{isamarkuptext}%
-\isacommand{consts}\ swap12\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a\ list{"}\isanewline
-\isacommand{recdef}\ swap12\ {"}{\isabraceleft}{\isabraceright}{"}\isanewline
-\ \ {"}swap12\ (x\#y\#zs)\ =\ y\#x\#zs{"}\isanewline
-\ \ {"}swap12\ zs\ \ \ \ \ \ \ =\ zs{"}%
+\isacommand{consts}\ swap\isadigit{1}\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
+\isacommand{recdef}\ swap\isadigit{1}\isadigit{2}\ {\isachardoublequote}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}swap\isadigit{1}\isadigit{2}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ y{\isacharhash}x{\isacharhash}zs{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}swap\isadigit{1}\isadigit{2}\ zs\ \ \ \ \ \ \ {\isacharequal}\ zs{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 For non-recursive functions the termination measure degenerates to the empty