merged

--- a/doc-src/Classes/Thy/Classes.thy	Thu Sep 23 17:22:45 2010 +0200
+++ b/doc-src/Classes/Thy/Classes.thy	Thu Sep 23 21:17:11 2010 +0200
@@ -601,18 +601,31 @@
   \noindent This maps to Haskell as follows:
 *}
 (*<*)code_include %invisible Haskell "Natural" -(*>*)
-text %quote {*@{code_stmts example (Haskell)}*}
+text %quote {*
+  \begin{typewriter}
+    @{code_stmts example (Haskell)}
+  \end{typewriter}
+*}
 
 text {*
   \noindent The code in SML has explicit dictionary passing:
 *}
-text %quote {*@{code_stmts example (SML)}*}
+text %quote {*
+  \begin{typewriter}
+    @{code_stmts example (SML)}
+  \end{typewriter}
+*}
+
 
 text {*
   \noindent In Scala, implicts are used as dictionaries:
 *}
 (*<*)code_include %invisible Scala "Natural" -(*>*)
-text %quote {*@{code_stmts example (Scala)}*}
+text %quote {*
+  \begin{typewriter}
+    @{code_stmts example (Scala)}
+  \end{typewriter}
+*}
 
 
 subsection {* Inspecting the type class universe *}

--- a/doc-src/Classes/Thy/document/Classes.tex	Thu Sep 23 17:22:45 2010 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex	Thu Sep 23 21:17:11 2010 +0200
@@ -1130,70 +1130,71 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}module Example where {\char123}\\
-\hspace*{0pt}\\
-\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}nat{\char95}aux ::~Integer -> Nat -> Nat;\\
-\hspace*{0pt}nat{\char95}aux i n = (if i <= 0 then n else nat{\char95}aux (i - 1) (Suc n));\\
-\hspace*{0pt}\\
-\hspace*{0pt}nat ::~Integer -> Nat;\\
-\hspace*{0pt}nat i = nat{\char95}aux i Zero{\char95}nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}class Semigroup a where {\char123}\\
-\hspace*{0pt} ~mult ::~a -> a -> a;\\
-\hspace*{0pt}{\char125};\\
-\hspace*{0pt}\\
-\hspace*{0pt}class (Semigroup a) => Monoidl a where {\char123}\\
-\hspace*{0pt} ~neutral ::~a;\\
-\hspace*{0pt}{\char125};\\
-\hspace*{0pt}\\
-\hspace*{0pt}class (Monoidl a) => Monoid a where {\char123}\\
-\hspace*{0pt}{\char125};\\
-\hspace*{0pt}\\
-\hspace*{0pt}class (Monoid a) => Group a where {\char123}\\
-\hspace*{0pt} ~inverse ::~a -> a;\\
-\hspace*{0pt}{\char125};\\
-\hspace*{0pt}\\
-\hspace*{0pt}pow{\char95}nat ::~forall a.~(Monoid a) => Nat -> a -> a;\\
-\hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\
-\hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\
-\hspace*{0pt}\\
-\hspace*{0pt}pow{\char95}int ::~forall a.~(Group a) => Integer -> a -> a;\\
-\hspace*{0pt}pow{\char95}int k x =\\
-\hspace*{0pt} ~(if 0 <= k then pow{\char95}nat (nat k) x\\
-\hspace*{0pt} ~~~else inverse (pow{\char95}nat (nat (negate k)) x));\\
-\hspace*{0pt}\\
-\hspace*{0pt}mult{\char95}int ::~Integer -> Integer -> Integer;\\
-\hspace*{0pt}mult{\char95}int i j = i + j;\\
-\hspace*{0pt}\\
-\hspace*{0pt}instance Semigroup Integer where {\char123}\\
-\hspace*{0pt} ~mult = mult{\char95}int;\\
-\hspace*{0pt}{\char125};\\
-\hspace*{0pt}\\
-\hspace*{0pt}neutral{\char95}int ::~Integer;\\
-\hspace*{0pt}neutral{\char95}int = 0;\\
-\hspace*{0pt}\\
-\hspace*{0pt}instance Monoidl Integer where {\char123}\\
-\hspace*{0pt} ~neutral = neutral{\char95}int;\\
-\hspace*{0pt}{\char125};\\
-\hspace*{0pt}\\
-\hspace*{0pt}instance Monoid Integer where {\char123}\\
-\hspace*{0pt}{\char125};\\
-\hspace*{0pt}\\
-\hspace*{0pt}inverse{\char95}int ::~Integer -> Integer;\\
-\hspace*{0pt}inverse{\char95}int i = negate i;\\
-\hspace*{0pt}\\
-\hspace*{0pt}instance Group Integer where {\char123}\\
-\hspace*{0pt} ~inverse = inverse{\char95}int;\\
-\hspace*{0pt}{\char125};\\
-\hspace*{0pt}\\
-\hspace*{0pt}example ::~Integer;\\
-\hspace*{0pt}example = pow{\char95}int 10 (-2);\\
-\hspace*{0pt}\\
-\hspace*{0pt}{\char125}%
+\begin{typewriter}
+    module\ Example\ where\ {\isacharbraceleft}\isanewline
+\isanewline
+data\ Nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ Nat{\isacharsemicolon}\isanewline
+\isanewline
+nat{\isacharunderscore}aux\ {\isacharcolon}{\isacharcolon}\ Integer\ {\isacharminus}{\isachargreater}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
+nat{\isacharunderscore}aux\ i\ n\ {\isacharequal}\ {\isacharparenleft}if\ i\ {\isacharless}{\isacharequal}\ {\isadigit{0}}\ then\ n\ else\ nat{\isacharunderscore}aux\ {\isacharparenleft}i\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+nat\ {\isacharcolon}{\isacharcolon}\ Integer\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
+nat\ i\ {\isacharequal}\ nat{\isacharunderscore}aux\ i\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline
+\isanewline
+class\ Semigroup\ a\ where\ {\isacharbraceleft}\isanewline
+\ \ mult\ {\isacharcolon}{\isacharcolon}\ a\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
+{\isacharbraceright}{\isacharsemicolon}\isanewline
+\isanewline
+class\ {\isacharparenleft}Semigroup\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Monoidl\ a\ where\ {\isacharbraceleft}\isanewline
+\ \ neutral\ {\isacharcolon}{\isacharcolon}\ a{\isacharsemicolon}\isanewline
+{\isacharbraceright}{\isacharsemicolon}\isanewline
+\isanewline
+class\ {\isacharparenleft}Monoidl\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Monoid\ a\ where\ {\isacharbraceleft}\isanewline
+{\isacharbraceright}{\isacharsemicolon}\isanewline
+\isanewline
+class\ {\isacharparenleft}Monoid\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Group\ a\ where\ {\isacharbraceleft}\isanewline
+\ \ inverse\ {\isacharcolon}{\isacharcolon}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
+{\isacharbraceright}{\isacharsemicolon}\isanewline
+\isanewline
+pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Monoid\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Nat\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
+pow{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ x\ {\isacharequal}\ neutral{\isacharsemicolon}\isanewline
+pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ mult\ x\ {\isacharparenleft}pow{\isacharunderscore}nat\ n\ x{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Group\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Integer\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
+pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\isanewline
+\ \ {\isacharparenleft}if\ {\isadigit{0}}\ {\isacharless}{\isacharequal}\ k\ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
+\ \ \ \ else\ inverse\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}negate\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+mult{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ Integer\ {\isacharminus}{\isachargreater}\ Integer\ {\isacharminus}{\isachargreater}\ Integer{\isacharsemicolon}\isanewline
+mult{\isacharunderscore}int\ i\ j\ {\isacharequal}\ i\ {\isacharplus}\ j{\isacharsemicolon}\isanewline
+\isanewline
+instance\ Semigroup\ Integer\ where\ {\isacharbraceleft}\isanewline
+\ \ mult\ {\isacharequal}\ mult{\isacharunderscore}int{\isacharsemicolon}\isanewline
+{\isacharbraceright}{\isacharsemicolon}\isanewline
+\isanewline
+neutral{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ Integer{\isacharsemicolon}\isanewline
+neutral{\isacharunderscore}int\ {\isacharequal}\ {\isadigit{0}}{\isacharsemicolon}\isanewline
+\isanewline
+instance\ Monoidl\ Integer\ where\ {\isacharbraceleft}\isanewline
+\ \ neutral\ {\isacharequal}\ neutral{\isacharunderscore}int{\isacharsemicolon}\isanewline
+{\isacharbraceright}{\isacharsemicolon}\isanewline
+\isanewline
+instance\ Monoid\ Integer\ where\ {\isacharbraceleft}\isanewline
+{\isacharbraceright}{\isacharsemicolon}\isanewline
+\isanewline
+inverse{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ Integer\ {\isacharminus}{\isachargreater}\ Integer{\isacharsemicolon}\isanewline
+inverse{\isacharunderscore}int\ i\ {\isacharequal}\ negate\ i{\isacharsemicolon}\isanewline
+\isanewline
+instance\ Group\ Integer\ where\ {\isacharbraceleft}\isanewline
+\ \ inverse\ {\isacharequal}\ inverse{\isacharunderscore}int{\isacharsemicolon}\isanewline
+{\isacharbraceright}{\isacharsemicolon}\isanewline
+\isanewline
+example\ {\isacharcolon}{\isacharcolon}\ Integer{\isacharsemicolon}\isanewline
+example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+{\isacharbraceright}\isanewline
+
+  \end{typewriter}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1216,86 +1217,87 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
-\hspace*{0pt} ~val nat{\char95}aux :~IntInf.int -> nat -> nat\\
-\hspace*{0pt} ~val nat :~IntInf.int -> nat\\
-\hspace*{0pt} ~type 'a semigroup\\
-\hspace*{0pt} ~val mult :~'a semigroup -> 'a -> 'a -> 'a\\
-\hspace*{0pt} ~type 'a monoidl\\
-\hspace*{0pt} ~val semigroup{\char95}monoidl :~'a monoidl -> 'a semigroup\\
-\hspace*{0pt} ~val neutral :~'a monoidl -> 'a\\
-\hspace*{0pt} ~type 'a monoid\\
-\hspace*{0pt} ~val monoidl{\char95}monoid :~'a monoid -> 'a monoidl\\
-\hspace*{0pt} ~type 'a group\\
-\hspace*{0pt} ~val monoid{\char95}group :~'a group -> 'a monoid\\
-\hspace*{0pt} ~val inverse :~'a group -> 'a -> 'a\\
-\hspace*{0pt} ~val pow{\char95}nat :~'a monoid -> nat -> 'a -> 'a\\
-\hspace*{0pt} ~val pow{\char95}int :~'a group -> IntInf.int -> 'a -> 'a\\
-\hspace*{0pt} ~val mult{\char95}int :~IntInf.int -> IntInf.int -> IntInf.int\\
-\hspace*{0pt} ~val semigroup{\char95}int :~IntInf.int semigroup\\
-\hspace*{0pt} ~val neutral{\char95}int :~IntInf.int\\
-\hspace*{0pt} ~val monoidl{\char95}int :~IntInf.int monoidl\\
-\hspace*{0pt} ~val monoid{\char95}int :~IntInf.int monoid\\
-\hspace*{0pt} ~val inverse{\char95}int :~IntInf.int -> IntInf.int\\
-\hspace*{0pt} ~val group{\char95}int :~IntInf.int group\\
-\hspace*{0pt} ~val example :~IntInf.int\\
-\hspace*{0pt}end = struct\\
-\hspace*{0pt}\\
-\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun nat{\char95}aux i n =\\
-\hspace*{0pt} ~(if IntInf.<= (i,~(0 :~IntInf.int)) then n\\
-\hspace*{0pt} ~~~else nat{\char95}aux (IntInf.- (i,~(1 :~IntInf.int))) (Suc n));\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun nat i = nat{\char95}aux i Zero{\char95}nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
-\hspace*{0pt}val mult = {\char35}mult :~'a semigroup -> 'a -> 'a -> 'a;\\
-\hspace*{0pt}\\
-\hspace*{0pt}type 'a monoidl = {\char123}semigroup{\char95}monoidl :~'a semigroup,~neutral :~'a{\char125};\\
-\hspace*{0pt}val semigroup{\char95}monoidl = {\char35}semigroup{\char95}monoidl :~'a monoidl -> 'a semigroup;\\
-\hspace*{0pt}val neutral = {\char35}neutral :~'a monoidl -> 'a;\\
-\hspace*{0pt}\\
-\hspace*{0pt}type 'a monoid = {\char123}monoidl{\char95}monoid :~'a monoidl{\char125};\\
-\hspace*{0pt}val monoidl{\char95}monoid = {\char35}monoidl{\char95}monoid :~'a monoid -> 'a monoidl;\\
-\hspace*{0pt}\\
-\hspace*{0pt}type 'a group = {\char123}monoid{\char95}group :~'a monoid,~inverse :~'a -> 'a{\char125};\\
-\hspace*{0pt}val monoid{\char95}group = {\char35}monoid{\char95}group :~'a group -> 'a monoid;\\
-\hspace*{0pt}val inverse = {\char35}inverse :~'a group -> 'a -> 'a;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\
-\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\
-\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun pow{\char95}int A{\char95}~k x =\\
-\hspace*{0pt} ~(if IntInf.<= ((0 :~IntInf.int),~k)\\
-\hspace*{0pt} ~~~then pow{\char95}nat (monoid{\char95}group A{\char95}) (nat k) x\\
-\hspace*{0pt} ~~~else inverse A{\char95}~(pow{\char95}nat (monoid{\char95}group A{\char95}) (nat (IntInf.{\char126}~k)) x));\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i,~j);\\
-\hspace*{0pt}\\
-\hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\
-\hspace*{0pt}\\
-\hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int);\\
-\hspace*{0pt}\\
-\hspace*{0pt}val monoidl{\char95}int =\\
-\hspace*{0pt} ~{\char123}semigroup{\char95}monoidl = semigroup{\char95}int,~neutral = neutral{\char95}int{\char125}~:\\
-\hspace*{0pt} ~IntInf.int monoidl;\\
-\hspace*{0pt}\\
-\hspace*{0pt}val monoid{\char95}int = {\char123}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:~IntInf.int monoid;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\
-\hspace*{0pt}\\
-\hspace*{0pt}val group{\char95}int = {\char123}monoid{\char95}group = monoid{\char95}int,~inverse = inverse{\char95}int{\char125}~:\\
-\hspace*{0pt} ~IntInf.int group;\\
-\hspace*{0pt}\\
-\hspace*{0pt}val example :~IntInf.int =\\
-\hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int);\\
-\hspace*{0pt}\\
-\hspace*{0pt}end;~(*struct Example*)%
+\begin{typewriter}
+    structure\ Example\ {\isacharcolon}\ sig\isanewline
+\ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline
+\ \ val\ nat{\isacharunderscore}aux\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ nat\isanewline
+\ \ val\ nat\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ nat\isanewline
+\ \ type\ {\isacharprime}a\ semigroup\isanewline
+\ \ val\ mult\ {\isacharcolon}\ {\isacharprime}a\ semigroup\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
+\ \ type\ {\isacharprime}a\ monoidl\isanewline
+\ \ val\ semigroup{\isacharunderscore}monoidl\ {\isacharcolon}\ {\isacharprime}a\ monoidl\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ semigroup\isanewline
+\ \ val\ neutral\ {\isacharcolon}\ {\isacharprime}a\ monoidl\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
+\ \ type\ {\isacharprime}a\ monoid\isanewline
+\ \ val\ monoidl{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ monoidl\isanewline
+\ \ type\ {\isacharprime}a\ group\isanewline
+\ \ val\ monoid{\isacharunderscore}group\ {\isacharcolon}\ {\isacharprime}a\ group\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ monoid\isanewline
+\ \ val\ inverse\ {\isacharcolon}\ {\isacharprime}a\ group\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
+\ \ val\ pow{\isacharunderscore}nat\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
+\ \ val\ pow{\isacharunderscore}int\ {\isacharcolon}\ {\isacharprime}a\ group\ {\isacharminus}{\isachargreater}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
+\ \ val\ mult{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ IntInf{\isachardot}int\isanewline
+\ \ val\ semigroup{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ semigroup\isanewline
+\ \ val\ neutral{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\isanewline
+\ \ val\ monoidl{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ monoidl\isanewline
+\ \ val\ monoid{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ monoid\isanewline
+\ \ val\ inverse{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ IntInf{\isachardot}int\isanewline
+\ \ val\ group{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ group\isanewline
+\ \ val\ example\ {\isacharcolon}\ IntInf{\isachardot}int\isanewline
+end\ {\isacharequal}\ struct\isanewline
+\isanewline
+datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat{\isacharsemicolon}\isanewline
+\isanewline
+fun\ nat{\isacharunderscore}aux\ i\ n\ {\isacharequal}\isanewline
+\ \ {\isacharparenleft}if\ IntInf{\isachardot}{\isacharless}{\isacharequal}\ {\isacharparenleft}i{\isacharcomma}\ {\isacharparenleft}{\isadigit{0}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}{\isacharparenright}\ then\ n\isanewline
+\ \ \ \ else\ nat{\isacharunderscore}aux\ {\isacharparenleft}IntInf{\isachardot}{\isacharminus}\ {\isacharparenleft}i{\isacharcomma}\ {\isacharparenleft}{\isadigit{1}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+fun\ nat\ i\ {\isacharequal}\ nat{\isacharunderscore}aux\ i\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline
+\isanewline
+type\ {\isacharprime}a\ semigroup\ {\isacharequal}\ {\isacharbraceleft}mult\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharbraceright}{\isacharsemicolon}\isanewline
+val\ mult\ {\isacharequal}\ {\isacharhash}mult\ {\isacharcolon}\ {\isacharprime}a\ semigroup\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharsemicolon}\isanewline
+\isanewline
+type\ {\isacharprime}a\ monoidl\ {\isacharequal}\ {\isacharbraceleft}semigroup{\isacharunderscore}monoidl\ {\isacharcolon}\ {\isacharprime}a\ semigroup{\isacharcomma}\ neutral\ {\isacharcolon}\ {\isacharprime}a{\isacharbraceright}{\isacharsemicolon}\isanewline
+val\ semigroup{\isacharunderscore}monoidl\ {\isacharequal}\ {\isacharhash}semigroup{\isacharunderscore}monoidl\ {\isacharcolon}\ {\isacharprime}a\ monoidl\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ semigroup{\isacharsemicolon}\isanewline
+val\ neutral\ {\isacharequal}\ {\isacharhash}neutral\ {\isacharcolon}\ {\isacharprime}a\ monoidl\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharsemicolon}\isanewline
+\isanewline
+type\ {\isacharprime}a\ monoid\ {\isacharequal}\ {\isacharbraceleft}monoidl{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ monoidl{\isacharbraceright}{\isacharsemicolon}\isanewline
+val\ monoidl{\isacharunderscore}monoid\ {\isacharequal}\ {\isacharhash}monoidl{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ monoidl{\isacharsemicolon}\isanewline
+\isanewline
+type\ {\isacharprime}a\ group\ {\isacharequal}\ {\isacharbraceleft}monoid{\isacharunderscore}group\ {\isacharcolon}\ {\isacharprime}a\ monoid{\isacharcomma}\ inverse\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharbraceright}{\isacharsemicolon}\isanewline
+val\ monoid{\isacharunderscore}group\ {\isacharequal}\ {\isacharhash}monoid{\isacharunderscore}group\ {\isacharcolon}\ {\isacharprime}a\ group\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ monoid{\isacharsemicolon}\isanewline
+val\ inverse\ {\isacharequal}\ {\isacharhash}inverse\ {\isacharcolon}\ {\isacharprime}a\ group\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharsemicolon}\isanewline
+\isanewline
+fun\ pow{\isacharunderscore}nat\ A{\isacharunderscore}\ Zero{\isacharunderscore}nat\ x\ {\isacharequal}\ neutral\ {\isacharparenleft}monoidl{\isacharunderscore}monoid\ A{\isacharunderscore}{\isacharparenright}\isanewline
+\ \ {\isacharbar}\ pow{\isacharunderscore}nat\ A{\isacharunderscore}\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\isanewline
+\ \ \ \ mult\ {\isacharparenleft}{\isacharparenleft}semigroup{\isacharunderscore}monoidl\ o\ monoidl{\isacharunderscore}monoid{\isacharparenright}\ A{\isacharunderscore}{\isacharparenright}\ x\ {\isacharparenleft}pow{\isacharunderscore}nat\ A{\isacharunderscore}\ n\ x{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+fun\ pow{\isacharunderscore}int\ A{\isacharunderscore}\ k\ x\ {\isacharequal}\isanewline
+\ \ {\isacharparenleft}if\ IntInf{\isachardot}{\isacharless}{\isacharequal}\ {\isacharparenleft}{\isacharparenleft}{\isadigit{0}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}{\isacharcomma}\ k{\isacharparenright}\isanewline
+\ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}monoid{\isacharunderscore}group\ A{\isacharunderscore}{\isacharparenright}\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
+\ \ \ \ else\ inverse\ A{\isacharunderscore}\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}monoid{\isacharunderscore}group\ A{\isacharunderscore}{\isacharparenright}\ {\isacharparenleft}nat\ {\isacharparenleft}IntInf{\isachardot}{\isachartilde}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+fun\ mult{\isacharunderscore}int\ i\ j\ {\isacharequal}\ IntInf{\isachardot}{\isacharplus}\ {\isacharparenleft}i{\isacharcomma}\ j{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+val\ semigroup{\isacharunderscore}int\ {\isacharequal}\ {\isacharbraceleft}mult\ {\isacharequal}\ mult{\isacharunderscore}int{\isacharbraceright}\ {\isacharcolon}\ IntInf{\isachardot}int\ semigroup{\isacharsemicolon}\isanewline
+\isanewline
+val\ neutral{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+val\ monoidl{\isacharunderscore}int\ {\isacharequal}\isanewline
+\ \ {\isacharbraceleft}semigroup{\isacharunderscore}monoidl\ {\isacharequal}\ semigroup{\isacharunderscore}int{\isacharcomma}\ neutral\ {\isacharequal}\ neutral{\isacharunderscore}int{\isacharbraceright}\ {\isacharcolon}\isanewline
+\ \ IntInf{\isachardot}int\ monoidl{\isacharsemicolon}\isanewline
+\isanewline
+val\ monoid{\isacharunderscore}int\ {\isacharequal}\ {\isacharbraceleft}monoidl{\isacharunderscore}monoid\ {\isacharequal}\ monoidl{\isacharunderscore}int{\isacharbraceright}\ {\isacharcolon}\ IntInf{\isachardot}int\ monoid{\isacharsemicolon}\isanewline
+\isanewline
+fun\ inverse{\isacharunderscore}int\ i\ {\isacharequal}\ IntInf{\isachardot}{\isachartilde}\ i{\isacharsemicolon}\isanewline
+\isanewline
+val\ group{\isacharunderscore}int\ {\isacharequal}\ {\isacharbraceleft}monoid{\isacharunderscore}group\ {\isacharequal}\ monoid{\isacharunderscore}int{\isacharcomma}\ inverse\ {\isacharequal}\ inverse{\isacharunderscore}int{\isacharbraceright}\ {\isacharcolon}\isanewline
+\ \ IntInf{\isachardot}int\ group{\isacharsemicolon}\isanewline
+\isanewline
+val\ example\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharequal}\isanewline
+\ \ pow{\isacharunderscore}int\ group{\isacharunderscore}int\ {\isacharparenleft}{\isadigit{1}}{\isadigit{0}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}\ {\isacharparenleft}{\isachartilde}{\isadigit{2}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline
+
+  \end{typewriter}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1331,76 +1333,77 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}object Example {\char123}\\
-\hspace*{0pt}\\
-\hspace*{0pt}abstract sealed class nat\\
-\hspace*{0pt}final case object Zero{\char95}nat extends nat\\
-\hspace*{0pt}final case class Suc(a:~nat) extends nat\\
-\hspace*{0pt}\\
-\hspace*{0pt}def nat{\char95}aux(i:~BigInt,~n:~nat):~nat =\\
-\hspace*{0pt} ~(if (i <= BigInt(0)) n else nat{\char95}aux(i - BigInt(1),~Suc(n)))\\
-\hspace*{0pt}\\
-\hspace*{0pt}def nat(i:~BigInt):~nat = nat{\char95}aux(i,~Zero{\char95}nat)\\
-\hspace*{0pt}\\
-\hspace*{0pt}trait semigroup[A] {\char123}\\
-\hspace*{0pt} ~val `Example.mult`:~(A,~A) => A\\
-\hspace*{0pt}{\char125}\\
-\hspace*{0pt}def mult[A](a:~A,~b:~A)(implicit A:~semigroup[A]):~A =\\
-\hspace*{0pt} ~A.`Example.mult`(a,~b)\\
-\hspace*{0pt}\\
-\hspace*{0pt}trait monoidl[A] extends semigroup[A] {\char123}\\
-\hspace*{0pt} ~val `Example.neutral`:~A\\
-\hspace*{0pt}{\char125}\\
-\hspace*{0pt}def neutral[A](implicit A:~monoidl[A]):~A = A.`Example.neutral`\\
-\hspace*{0pt}\\
-\hspace*{0pt}trait monoid[A] extends monoidl[A] {\char123}\\
-\hspace*{0pt}{\char125}\\
-\hspace*{0pt}\\
-\hspace*{0pt}trait group[A] extends monoid[A] {\char123}\\
-\hspace*{0pt} ~val `Example.inverse`:~A => A\\
-\hspace*{0pt}{\char125}\\
-\hspace*{0pt}def inverse[A](a:~A)(implicit A:~group[A]):~A = A.`Example.inverse`(a)\\
-\hspace*{0pt}\\
-\hspace*{0pt}def pow{\char95}nat[A:~monoid](xa0:~nat,~x:~A):~A = (xa0,~x) match {\char123}\\
-\hspace*{0pt} ~case (Zero{\char95}nat,~x) => neutral[A]\\
-\hspace*{0pt} ~case (Suc(n),~x) => mult[A](x,~pow{\char95}nat[A](n,~x))\\
-\hspace*{0pt}{\char125}\\
-\hspace*{0pt}\\
-\hspace*{0pt}def pow{\char95}int[A:~group](k:~BigInt,~x:~A):~A =\\
-\hspace*{0pt} ~(if (BigInt(0) <= k) pow{\char95}nat[A](nat(k),~x)\\
-\hspace*{0pt} ~~~else inverse[A](pow{\char95}nat[A](nat((- k)),~x)))\\
-\hspace*{0pt}\\
-\hspace*{0pt}def mult{\char95}int(i:~BigInt,~j:~BigInt):~BigInt = i + j\\
-\hspace*{0pt}\\
-\hspace*{0pt}implicit def semigroup{\char95}int:~semigroup[BigInt] = new semigroup[BigInt] {\char123}\\
-\hspace*{0pt} ~val `Example.mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\
-\hspace*{0pt}{\char125}\\
-\hspace*{0pt}\\
-\hspace*{0pt}def neutral{\char95}int:~BigInt = BigInt(0)\\
-\hspace*{0pt}\\
-\hspace*{0pt}implicit def monoidl{\char95}int:~monoidl[BigInt] = new monoidl[BigInt] {\char123}\\
-\hspace*{0pt} ~val `Example.neutral` = neutral{\char95}int\\
-\hspace*{0pt} ~val `Example.mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\
-\hspace*{0pt}{\char125}\\
-\hspace*{0pt}\\
-\hspace*{0pt}implicit def monoid{\char95}int:~monoid[BigInt] = new monoid[BigInt] {\char123}\\
-\hspace*{0pt} ~val `Example.neutral` = neutral{\char95}int\\
-\hspace*{0pt} ~val `Example.mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\
-\hspace*{0pt}{\char125}\\
-\hspace*{0pt}\\
-\hspace*{0pt}def inverse{\char95}int(i:~BigInt):~BigInt = (- i)\\
-\hspace*{0pt}\\
-\hspace*{0pt}implicit def group{\char95}int:~group[BigInt] = new group[BigInt] {\char123}\\
-\hspace*{0pt} ~val `Example.inverse` = (a:~BigInt) => inverse{\char95}int(a)\\
-\hspace*{0pt} ~val `Example.neutral` = neutral{\char95}int\\
-\hspace*{0pt} ~val `Example.mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\
-\hspace*{0pt}{\char125}\\
-\hspace*{0pt}\\
-\hspace*{0pt}def example:~BigInt = pow{\char95}int[BigInt](BigInt(10),~BigInt(- 2))\\
-\hspace*{0pt}\\
-\hspace*{0pt}{\char125}~/* object Example */%
+\begin{typewriter}
+    object\ Example\ {\isacharbraceleft}\isanewline
+\isanewline
+abstract\ sealed\ class\ nat\isanewline
+final\ case\ object\ Zero{\isacharunderscore}nat\ extends\ nat\isanewline
+final\ case\ class\ Suc{\isacharparenleft}a{\isacharcolon}\ nat{\isacharparenright}\ extends\ nat\isanewline
+\isanewline
+def\ nat{\isacharunderscore}aux{\isacharparenleft}i{\isacharcolon}\ BigInt{\isacharcomma}\ n{\isacharcolon}\ nat{\isacharparenright}{\isacharcolon}\ nat\ {\isacharequal}\isanewline
+\ \ {\isacharparenleft}if\ {\isacharparenleft}i\ {\isacharless}{\isacharequal}\ BigInt{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isacharparenright}\ n\ else\ nat{\isacharunderscore}aux{\isacharparenleft}i\ {\isacharminus}\ BigInt{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharcomma}\ Suc{\isacharparenleft}n{\isacharparenright}{\isacharparenright}{\isacharparenright}\isanewline
+\isanewline
+def\ nat{\isacharparenleft}i{\isacharcolon}\ BigInt{\isacharparenright}{\isacharcolon}\ nat\ {\isacharequal}\ nat{\isacharunderscore}aux{\isacharparenleft}i{\isacharcomma}\ Zero{\isacharunderscore}nat{\isacharparenright}\isanewline
+\isanewline
+trait\ semigroup{\isacharbrackleft}A{\isacharbrackright}\ {\isacharbraceleft}\isanewline
+\ \ val\ {\isacharbackquote}Example{\isachardot}mult{\isacharbackquote}{\isacharcolon}\ {\isacharparenleft}A{\isacharcomma}\ A{\isacharparenright}\ {\isacharequal}{\isachargreater}\ A\isanewline
+{\isacharbraceright}\isanewline
+def\ mult{\isacharbrackleft}A{\isacharbrackright}{\isacharparenleft}a{\isacharcolon}\ A{\isacharcomma}\ b{\isacharcolon}\ A{\isacharparenright}{\isacharparenleft}implicit\ A{\isacharcolon}\ semigroup{\isacharbrackleft}A{\isacharbrackright}{\isacharparenright}{\isacharcolon}\ A\ {\isacharequal}\isanewline
+\ \ A{\isachardot}{\isacharbackquote}Example{\isachardot}mult{\isacharbackquote}{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\isanewline
+\isanewline
+trait\ monoidl{\isacharbrackleft}A{\isacharbrackright}\ extends\ semigroup{\isacharbrackleft}A{\isacharbrackright}\ {\isacharbraceleft}\isanewline
+\ \ val\ {\isacharbackquote}Example{\isachardot}neutral{\isacharbackquote}{\isacharcolon}\ A\isanewline
+{\isacharbraceright}\isanewline
+def\ neutral{\isacharbrackleft}A{\isacharbrackright}{\isacharparenleft}implicit\ A{\isacharcolon}\ monoidl{\isacharbrackleft}A{\isacharbrackright}{\isacharparenright}{\isacharcolon}\ A\ {\isacharequal}\ A{\isachardot}{\isacharbackquote}Example{\isachardot}neutral{\isacharbackquote}\isanewline
+\isanewline
+trait\ monoid{\isacharbrackleft}A{\isacharbrackright}\ extends\ monoidl{\isacharbrackleft}A{\isacharbrackright}\ {\isacharbraceleft}\isanewline
+{\isacharbraceright}\isanewline
+\isanewline
+trait\ group{\isacharbrackleft}A{\isacharbrackright}\ extends\ monoid{\isacharbrackleft}A{\isacharbrackright}\ {\isacharbraceleft}\isanewline
+\ \ val\ {\isacharbackquote}Example{\isachardot}inverse{\isacharbackquote}{\isacharcolon}\ A\ {\isacharequal}{\isachargreater}\ A\isanewline
+{\isacharbraceright}\isanewline
+def\ inverse{\isacharbrackleft}A{\isacharbrackright}{\isacharparenleft}a{\isacharcolon}\ A{\isacharparenright}{\isacharparenleft}implicit\ A{\isacharcolon}\ group{\isacharbrackleft}A{\isacharbrackright}{\isacharparenright}{\isacharcolon}\ A\ {\isacharequal}\ A{\isachardot}{\isacharbackquote}Example{\isachardot}inverse{\isacharbackquote}{\isacharparenleft}a{\isacharparenright}\isanewline
+\isanewline
+def\ pow{\isacharunderscore}nat{\isacharbrackleft}A{\isacharcolon}\ monoid{\isacharbrackright}{\isacharparenleft}xa{\isadigit{0}}{\isacharcolon}\ nat{\isacharcomma}\ x{\isacharcolon}\ A{\isacharparenright}{\isacharcolon}\ A\ {\isacharequal}\ {\isacharparenleft}xa{\isadigit{0}}{\isacharcomma}\ x{\isacharparenright}\ match\ {\isacharbraceleft}\isanewline
+\ \ case\ {\isacharparenleft}Zero{\isacharunderscore}nat{\isacharcomma}\ x{\isacharparenright}\ {\isacharequal}{\isachargreater}\ neutral{\isacharbrackleft}A{\isacharbrackright}\isanewline
+\ \ case\ {\isacharparenleft}Suc{\isacharparenleft}n{\isacharparenright}{\isacharcomma}\ x{\isacharparenright}\ {\isacharequal}{\isachargreater}\ mult{\isacharbrackleft}A{\isacharbrackright}{\isacharparenleft}x{\isacharcomma}\ pow{\isacharunderscore}nat{\isacharbrackleft}A{\isacharbrackright}{\isacharparenleft}n{\isacharcomma}\ x{\isacharparenright}{\isacharparenright}\isanewline
+{\isacharbraceright}\isanewline
+\isanewline
+def\ pow{\isacharunderscore}int{\isacharbrackleft}A{\isacharcolon}\ group{\isacharbrackright}{\isacharparenleft}k{\isacharcolon}\ BigInt{\isacharcomma}\ x{\isacharcolon}\ A{\isacharparenright}{\isacharcolon}\ A\ {\isacharequal}\isanewline
+\ \ {\isacharparenleft}if\ {\isacharparenleft}BigInt{\isacharparenleft}{\isadigit{0}}{\isacharparenright}\ {\isacharless}{\isacharequal}\ k{\isacharparenright}\ pow{\isacharunderscore}nat{\isacharbrackleft}A{\isacharbrackright}{\isacharparenleft}nat{\isacharparenleft}k{\isacharparenright}{\isacharcomma}\ x{\isacharparenright}\isanewline
+\ \ \ \ else\ inverse{\isacharbrackleft}A{\isacharbrackright}{\isacharparenleft}pow{\isacharunderscore}nat{\isacharbrackleft}A{\isacharbrackright}{\isacharparenleft}nat{\isacharparenleft}{\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}{\isacharcomma}\ x{\isacharparenright}{\isacharparenright}{\isacharparenright}\isanewline
+\isanewline
+def\ mult{\isacharunderscore}int{\isacharparenleft}i{\isacharcolon}\ BigInt{\isacharcomma}\ j{\isacharcolon}\ BigInt{\isacharparenright}{\isacharcolon}\ BigInt\ {\isacharequal}\ i\ {\isacharplus}\ j\isanewline
+\isanewline
+implicit\ def\ semigroup{\isacharunderscore}int{\isacharcolon}\ semigroup{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharequal}\ new\ semigroup{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharbraceleft}\isanewline
+\ \ val\ {\isacharbackquote}Example{\isachardot}mult{\isacharbackquote}\ {\isacharequal}\ {\isacharparenleft}a{\isacharcolon}\ BigInt{\isacharcomma}\ b{\isacharcolon}\ BigInt{\isacharparenright}\ {\isacharequal}{\isachargreater}\ mult{\isacharunderscore}int{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\isanewline
+{\isacharbraceright}\isanewline
+\isanewline
+def\ neutral{\isacharunderscore}int{\isacharcolon}\ BigInt\ {\isacharequal}\ BigInt{\isacharparenleft}{\isadigit{0}}{\isacharparenright}\isanewline
+\isanewline
+implicit\ def\ monoidl{\isacharunderscore}int{\isacharcolon}\ monoidl{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharequal}\ new\ monoidl{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharbraceleft}\isanewline
+\ \ val\ {\isacharbackquote}Example{\isachardot}neutral{\isacharbackquote}\ {\isacharequal}\ neutral{\isacharunderscore}int\isanewline
+\ \ val\ {\isacharbackquote}Example{\isachardot}mult{\isacharbackquote}\ {\isacharequal}\ {\isacharparenleft}a{\isacharcolon}\ BigInt{\isacharcomma}\ b{\isacharcolon}\ BigInt{\isacharparenright}\ {\isacharequal}{\isachargreater}\ mult{\isacharunderscore}int{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\isanewline
+{\isacharbraceright}\isanewline
+\isanewline
+implicit\ def\ monoid{\isacharunderscore}int{\isacharcolon}\ monoid{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharequal}\ new\ monoid{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharbraceleft}\isanewline
+\ \ val\ {\isacharbackquote}Example{\isachardot}neutral{\isacharbackquote}\ {\isacharequal}\ neutral{\isacharunderscore}int\isanewline
+\ \ val\ {\isacharbackquote}Example{\isachardot}mult{\isacharbackquote}\ {\isacharequal}\ {\isacharparenleft}a{\isacharcolon}\ BigInt{\isacharcomma}\ b{\isacharcolon}\ BigInt{\isacharparenright}\ {\isacharequal}{\isachargreater}\ mult{\isacharunderscore}int{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\isanewline
+{\isacharbraceright}\isanewline
+\isanewline
+def\ inverse{\isacharunderscore}int{\isacharparenleft}i{\isacharcolon}\ BigInt{\isacharparenright}{\isacharcolon}\ BigInt\ {\isacharequal}\ {\isacharparenleft}{\isacharminus}\ i{\isacharparenright}\isanewline
+\isanewline
+implicit\ def\ group{\isacharunderscore}int{\isacharcolon}\ group{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharequal}\ new\ group{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharbraceleft}\isanewline
+\ \ val\ {\isacharbackquote}Example{\isachardot}inverse{\isacharbackquote}\ {\isacharequal}\ {\isacharparenleft}a{\isacharcolon}\ BigInt{\isacharparenright}\ {\isacharequal}{\isachargreater}\ inverse{\isacharunderscore}int{\isacharparenleft}a{\isacharparenright}\isanewline
+\ \ val\ {\isacharbackquote}Example{\isachardot}neutral{\isacharbackquote}\ {\isacharequal}\ neutral{\isacharunderscore}int\isanewline
+\ \ val\ {\isacharbackquote}Example{\isachardot}mult{\isacharbackquote}\ {\isacharequal}\ {\isacharparenleft}a{\isacharcolon}\ BigInt{\isacharcomma}\ b{\isacharcolon}\ BigInt{\isacharparenright}\ {\isacharequal}{\isachargreater}\ mult{\isacharunderscore}int{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\isanewline
+{\isacharbraceright}\isanewline
+\isanewline
+def\ example{\isacharcolon}\ BigInt\ {\isacharequal}\ pow{\isacharunderscore}int{\isacharbrackleft}BigInt{\isacharbrackright}{\isacharparenleft}BigInt{\isacharparenleft}{\isadigit{1}}{\isadigit{0}}{\isacharparenright}{\isacharcomma}\ BigInt{\isacharparenleft}{\isacharminus}\ {\isadigit{2}}{\isacharparenright}{\isacharparenright}\isanewline
+\isanewline
+{\isacharbraceright}\ {\isacharslash}{\isacharasterisk}\ object\ Example\ {\isacharasterisk}{\isacharslash}\isanewline
+
+  \end{typewriter}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %

--- a/doc-src/Classes/style.sty	Thu Sep 23 17:22:45 2010 +0200
+++ b/doc-src/Classes/style.sty	Thu Sep 23 21:17:11 2010 +0200
@@ -16,6 +16,7 @@
 
 %% typographic conventions
 \newcommand{\qt}[1]{``{#1}''}
+\newcommand{\ditem}[1]{\item[\isastyletext #1]}
 
 %% quote environment
 \isakeeptag{quote}
@@ -26,6 +27,12 @@
 \renewcommand{\endisatagquote}{\end{quote}}
 \newcommand{\quotebreak}{\\[1.2ex]}
 
+%% typewriter text
+\newenvironment{typewriter}{\renewcommand{\isadigit}[1]{{##1}}%
+\parindent0pt%
+\fontsize{9pt}{0pt}%
+\isabellestyle{tt}\isastyle}{}
+
 %% presentation
 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
 

--- a/doc-src/Codegen/Thy/Adaptation.thy	Thu Sep 23 17:22:45 2010 +0200
+++ b/doc-src/Codegen/Thy/Adaptation.thy	Thu Sep 23 21:17:11 2010 +0200
@@ -175,7 +175,11 @@
 code_const %invisible True and False and "op \<and>" and Not
   (SML and and and)
 (*>*)
-text %quote {*@{code_stmts in_interval (SML)}*}
+text %quote {*
+  \begin{typewriter}
+    @{code_stmts in_interval (SML)}
+  \end{typewriter}
+*}
 
 text {*
   \noindent Though this is correct code, it is a little bit
@@ -204,7 +208,11 @@
   placeholder for the type constructor's (the constant's) arguments.
 *}
 
-text %quote {*@{code_stmts in_interval (SML)}*}
+text %quote {*
+  \begin{typewriter}
+    @{code_stmts in_interval (SML)}
+  \end{typewriter}
+*}
 
 text {*
   \noindent This still is not perfect: the parentheses around the
@@ -217,7 +225,11 @@
 code_const %quotett "op \<and>"
   (SML infixl 1 "andalso")
 
-text %quote {*@{code_stmts in_interval (SML)}*}
+text %quote {*
+  \begin{typewriter}
+    @{code_stmts in_interval (SML)}
+  \end{typewriter}
+*}
 
 text {*
   \noindent The attentive reader may ask how we assert that no

--- a/doc-src/Codegen/Thy/Foundations.thy	Thu Sep 23 17:22:45 2010 +0200
+++ b/doc-src/Codegen/Thy/Foundations.thy	Thu Sep 23 21:17:11 2010 +0200
@@ -161,7 +161,11 @@
   is determined syntactically.  The resulting code:
 *}
 
-text %quote {*@{code_stmts dequeue (consts) dequeue (Haskell)}*}
+text %quote {*
+  \begin{typewriter}
+    @{code_stmts dequeue (consts) dequeue (Haskell)}
+  \end{typewriter}
+*}
 
 text {*
   \noindent You may note that the equality test @{term "xs = []"} has
@@ -215,7 +219,11 @@
   equality check, as can be seen in the corresponding @{text SML} code:
 *}
 
-text %quote {*@{code_stmts collect_duplicates (SML)}*}
+text %quote {*
+  \begin{typewriter}
+    @{code_stmts collect_duplicates (SML)}
+  \end{typewriter}
+*}
 
 text {*
   \noindent Obviously, polymorphic equality is implemented the Haskell
@@ -251,7 +259,11 @@
   for the pattern @{term "AQueue [] []"}:
 *}
 
-text %quote {*@{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}*}
+text %quote {*
+  \begin{typewriter}
+    @{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}
+  \end{typewriter}
+*}
 
 text {*
   \noindent In some cases it is desirable to have this
@@ -290,7 +302,11 @@
   exception at the appropriate position:
 *}
 
-text %quote {*@{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}*}
+text %quote {*
+  \begin{typewriter}
+    @{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}
+  \end{typewriter}
+*}
 
 text {*
   \noindent This feature however is rarely needed in practice.  Note

--- a/doc-src/Codegen/Thy/Further.thy	Thu Sep 23 17:22:45 2010 +0200
+++ b/doc-src/Codegen/Thy/Further.thy	Thu Sep 23 21:17:11 2010 +0200
@@ -112,7 +112,11 @@
   After this setup procedure, code generation can continue as usual:
 *}
 
-text %quote {*@{code_stmts funpows (consts) Nat.funpow funpows (Haskell)}*}
+text %quote {*
+  \begin{typewriter}
+    @{code_stmts funpows (consts) Nat.funpow funpows (Haskell)}
+  \end{typewriter}
+*}
 
 
 subsection {* Imperative data structures *}

--- a/doc-src/Codegen/Thy/Introduction.thy	Thu Sep 23 17:22:45 2010 +0200
+++ b/doc-src/Codegen/Thy/Introduction.thy	Thu Sep 23 21:17:11 2010 +0200
@@ -70,7 +70,11 @@
 
 text {* \noindent resulting in the following code: *}
 
-text %quote {*@{code_stmts empty enqueue dequeue (SML)}*}
+text %quote {*
+  \begin{typewriter}
+    @{code_stmts empty enqueue dequeue (SML)}
+  \end{typewriter}
+*}
 
 text {*
   \noindent The @{command_def export_code} command takes a
@@ -91,7 +95,11 @@
   \noindent This is the corresponding code:
 *}
 
-text %quote {*@{code_stmts empty enqueue dequeue (Haskell)}*}
+text %quote {*
+  \begin{typewriter}
+    @{code_stmts empty enqueue dequeue (Haskell)}
+  \end{typewriter}
+*}
 
 text {*
   \noindent For more details about @{command export_code} see
@@ -164,7 +172,11 @@
   native classes:
 *}
 
-text %quote {*@{code_stmts bexp (Haskell)}*}
+text %quote {*
+  \begin{typewriter}
+    @{code_stmts bexp (Haskell)}
+  \end{typewriter}
+*}
 
 text {*
   \noindent This is a convenient place to show how explicit dictionary
@@ -172,7 +184,11 @@
   @{text SML}:
 *}
 
-text %quote {*@{code_stmts bexp (SML)}*}
+text %quote {*
+  \begin{typewriter}
+    @{code_stmts bexp (SML)}
+  \end{typewriter}
+*}
 
 text {*
   \noindent Note the parameters with trailing underscore (@{verbatim

--- a/doc-src/Codegen/Thy/Refinement.thy	Thu Sep 23 17:22:45 2010 +0200
+++ b/doc-src/Codegen/Thy/Refinement.thy	Thu Sep 23 21:17:11 2010 +0200
@@ -31,7 +31,11 @@
   to two recursive calls:
 *}
 
-text %quote {*@{code_stmts fib (consts) fib (Haskell)}*}
+text %quote {*
+  \begin{typewriter}
+    @{code_stmts fib (consts) fib (Haskell)}
+  \end{typewriter}
+*}
 
 text {*
   \noindent A more efficient implementation would use dynamic
@@ -67,7 +71,11 @@
   \noindent The resulting code shows only linear growth of runtime:
 *}
 
-text %quote {*@{code_stmts fib (consts) fib fib_step (Haskell)}*}
+text %quote {*
+  \begin{typewriter}
+    @{code_stmts fib (consts) fib fib_step (Haskell)}
+  \end{typewriter}
+*}
 
 
 subsection {* Datatype refinement *}
@@ -153,7 +161,11 @@
   \noindent The resulting code looks as expected:
 *}
 
-text %quote {*@{code_stmts empty enqueue dequeue (SML)}*}
+text %quote {*
+  \begin{typewriter}
+    @{code_stmts empty enqueue dequeue (SML)}
+  \end{typewriter}
+*}
 
 text {*
   The same techniques can also be applied to types which are not
@@ -248,7 +260,9 @@
 *}
 
 text %quote {*
-  @{code_stmts Dlist.empty Dlist.insert Dlist.remove list_of_dlist (Haskell)}
+  \begin{typewriter}
+    @{code_stmts Dlist.empty Dlist.insert Dlist.remove list_of_dlist (Haskell)}
+  \end{typewriter}
 *} (*(types) dlist (consts) dempty dinsert dremove list_of List.member insert remove *)
 
 text {*

--- a/doc-src/Codegen/Thy/document/Adaptation.tex	Thu Sep 23 17:22:45 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex	Thu Sep 23 21:17:11 2010 +0200
@@ -235,34 +235,35 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
-\hspace*{0pt} ~datatype boola = True | False\\
-\hspace*{0pt} ~val conj :~boola -> boola -> boola\\
-\hspace*{0pt} ~val less{\char95}nat :~nat -> nat -> boola\\
-\hspace*{0pt} ~val less{\char95}eq{\char95}nat :~nat -> nat -> boola\\
-\hspace*{0pt} ~val in{\char95}interval :~nat * nat -> nat -> boola\\
-\hspace*{0pt}end = struct\\
-\hspace*{0pt}\\
-\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}datatype boola = True | False;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun conj p True = p\\
-\hspace*{0pt} ~| conj p False = False\\
-\hspace*{0pt} ~| conj True p = p\\
-\hspace*{0pt} ~| conj False p = False;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = False\\
-\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = True;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun in{\char95}interval (k,~l) n = conj (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\
-\hspace*{0pt}\\
-\hspace*{0pt}end;~(*struct Example*)%
+\begin{typewriter}
+    structure\ Example\ {\isacharcolon}\ sig\isanewline
+\ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline
+\ \ datatype\ boola\ {\isacharequal}\ True\ {\isacharbar}\ False\isanewline
+\ \ val\ conj\ {\isacharcolon}\ boola\ {\isacharminus}{\isachargreater}\ boola\ {\isacharminus}{\isachargreater}\ boola\isanewline
+\ \ val\ less{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ boola\isanewline
+\ \ val\ less{\isacharunderscore}eq{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ boola\isanewline
+\ \ val\ in{\isacharunderscore}interval\ {\isacharcolon}\ nat\ {\isacharasterisk}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ boola\isanewline
+end\ {\isacharequal}\ struct\isanewline
+\isanewline
+datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat{\isacharsemicolon}\isanewline
+\isanewline
+datatype\ boola\ {\isacharequal}\ True\ {\isacharbar}\ False{\isacharsemicolon}\isanewline
+\isanewline
+fun\ conj\ p\ True\ {\isacharequal}\ p\isanewline
+\ \ {\isacharbar}\ conj\ p\ False\ {\isacharequal}\ False\isanewline
+\ \ {\isacharbar}\ conj\ True\ p\ {\isacharequal}\ p\isanewline
+\ \ {\isacharbar}\ conj\ False\ p\ {\isacharequal}\ False{\isacharsemicolon}\isanewline
+\isanewline
+fun\ less{\isacharunderscore}nat\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ less{\isacharunderscore}eq{\isacharunderscore}nat\ m\ n\isanewline
+\ \ {\isacharbar}\ less{\isacharunderscore}nat\ n\ Zero{\isacharunderscore}nat\ {\isacharequal}\ False\isanewline
+and\ less{\isacharunderscore}eq{\isacharunderscore}nat\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n\ {\isacharequal}\ less{\isacharunderscore}nat\ m\ n\isanewline
+\ \ {\isacharbar}\ less{\isacharunderscore}eq{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ n\ {\isacharequal}\ True{\isacharsemicolon}\isanewline
+\isanewline
+fun\ in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isacharequal}\ conj\ {\isacharparenleft}less{\isacharunderscore}eq{\isacharunderscore}nat\ k\ n{\isacharparenright}\ {\isacharparenleft}less{\isacharunderscore}eq{\isacharunderscore}nat\ n\ l{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline
+
+  \end{typewriter}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -320,25 +321,26 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
-\hspace*{0pt} ~val less{\char95}nat :~nat -> nat -> bool\\
-\hspace*{0pt} ~val less{\char95}eq{\char95}nat :~nat -> nat -> bool\\
-\hspace*{0pt} ~val in{\char95}interval :~nat * nat -> nat -> bool\\
-\hspace*{0pt}end = struct\\
-\hspace*{0pt}\\
-\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
-\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun in{\char95}interval (k,~l) n = (less{\char95}eq{\char95}nat k n) andalso (less{\char95}eq{\char95}nat n l);\\
-\hspace*{0pt}\\
-\hspace*{0pt}end;~(*struct Example*)%
+\begin{typewriter}
+    structure\ Example\ {\isacharcolon}\ sig\isanewline
+\ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline
+\ \ val\ less{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline
+\ \ val\ less{\isacharunderscore}eq{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline
+\ \ val\ in{\isacharunderscore}interval\ {\isacharcolon}\ nat\ {\isacharasterisk}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline
+end\ {\isacharequal}\ struct\isanewline
+\isanewline
+datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat{\isacharsemicolon}\isanewline
+\isanewline
+fun\ less{\isacharunderscore}nat\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ less{\isacharunderscore}eq{\isacharunderscore}nat\ m\ n\isanewline
+\ \ {\isacharbar}\ less{\isacharunderscore}nat\ n\ Zero{\isacharunderscore}nat\ {\isacharequal}\ false\isanewline
+and\ less{\isacharunderscore}eq{\isacharunderscore}nat\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n\ {\isacharequal}\ less{\isacharunderscore}nat\ m\ n\isanewline
+\ \ {\isacharbar}\ less{\isacharunderscore}eq{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ n\ {\isacharequal}\ true{\isacharsemicolon}\isanewline
+\isanewline
+fun\ in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isacharequal}\ {\isacharparenleft}less{\isacharunderscore}eq{\isacharunderscore}nat\ k\ n{\isacharparenright}\ andalso\ {\isacharparenleft}less{\isacharunderscore}eq{\isacharunderscore}nat\ n\ l{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline
+
+  \end{typewriter}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -380,25 +382,26 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
-\hspace*{0pt} ~val less{\char95}nat :~nat -> nat -> bool\\
-\hspace*{0pt} ~val less{\char95}eq{\char95}nat :~nat -> nat -> bool\\
-\hspace*{0pt} ~val in{\char95}interval :~nat * nat -> nat -> bool\\
-\hspace*{0pt}end = struct\\
-\hspace*{0pt}\\
-\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
-\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun in{\char95}interval (k,~l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\
-\hspace*{0pt}\\
-\hspace*{0pt}end;~(*struct Example*)%
+\begin{typewriter}
+    structure\ Example\ {\isacharcolon}\ sig\isanewline
+\ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline
+\ \ val\ less{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline
+\ \ val\ less{\isacharunderscore}eq{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline
+\ \ val\ in{\isacharunderscore}interval\ {\isacharcolon}\ nat\ {\isacharasterisk}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline
+end\ {\isacharequal}\ struct\isanewline
+\isanewline
+datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat{\isacharsemicolon}\isanewline
+\isanewline
+fun\ less{\isacharunderscore}nat\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ less{\isacharunderscore}eq{\isacharunderscore}nat\ m\ n\isanewline
+\ \ {\isacharbar}\ less{\isacharunderscore}nat\ n\ Zero{\isacharunderscore}nat\ {\isacharequal}\ false\isanewline
+and\ less{\isacharunderscore}eq{\isacharunderscore}nat\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n\ {\isacharequal}\ less{\isacharunderscore}nat\ m\ n\isanewline
+\ \ {\isacharbar}\ less{\isacharunderscore}eq{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ n\ {\isacharequal}\ true{\isacharsemicolon}\isanewline
+\isanewline
+fun\ in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isacharequal}\ less{\isacharunderscore}eq{\isacharunderscore}nat\ k\ n\ andalso\ less{\isacharunderscore}eq{\isacharunderscore}nat\ n\ l{\isacharsemicolon}\isanewline
+\isanewline
+end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline
+
+  \end{typewriter}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %

--- a/doc-src/Codegen/Thy/document/Foundations.tex	Thu Sep 23 17:22:45 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Foundations.tex	Thu Sep 23 21:17:11 2010 +0200
@@ -245,13 +245,13 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
-\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
-\hspace*{0pt}dequeue (AQueue xs []) =\\
-\hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\
-\hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));%
+\begin{typewriter}
+    dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Maybe\ a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline
+dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Just\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isacharsemicolon}\isanewline
+dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ {\isacharparenleft}if\ null\ xs\ then\ {\isacharparenleft}Nothing{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
+\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}reverse\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}
+  \end{typewriter}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -347,33 +347,34 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt} ~type 'a equal\\
-\hspace*{0pt} ~val equal :~'a equal -> 'a -> 'a -> bool\\
-\hspace*{0pt} ~val eq :~'a equal -> 'a -> 'a -> bool\\
-\hspace*{0pt} ~val member :~'a equal -> 'a list -> 'a -> bool\\
-\hspace*{0pt} ~val collect{\char95}duplicates :\\
-\hspace*{0pt} ~~~'a equal -> 'a list -> 'a list -> 'a list -> 'a list\\
-\hspace*{0pt}end = struct\\
-\hspace*{0pt}\\
-\hspace*{0pt}type 'a equal = {\char123}equal :~'a -> 'a -> bool{\char125};\\
-\hspace*{0pt}val equal = {\char35}equal :~'a equal -> 'a -> 'a -> bool;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun eq A{\char95}~a b = equal A{\char95}~a b;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun member A{\char95}~[] y = false\\
-\hspace*{0pt} ~| member A{\char95}~(x ::~xs) y = eq A{\char95}~x y orelse member A{\char95}~xs y;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\
-\hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\
-\hspace*{0pt} ~~~(if member A{\char95}~xs z\\
-\hspace*{0pt} ~~~~~then (if member A{\char95}~ys z then collect{\char95}duplicates A{\char95}~xs ys zs\\
-\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\
-\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\
-\hspace*{0pt}\\
-\hspace*{0pt}end;~(*struct Example*)%
+\begin{typewriter}
+    structure\ Example\ {\isacharcolon}\ sig\isanewline
+\ \ type\ {\isacharprime}a\ equal\isanewline
+\ \ val\ equal\ {\isacharcolon}\ {\isacharprime}a\ equal\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ bool\isanewline
+\ \ val\ eq\ {\isacharcolon}\ {\isacharprime}a\ equal\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ bool\isanewline
+\ \ val\ member\ {\isacharcolon}\ {\isacharprime}a\ equal\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ bool\isanewline
+\ \ val\ collect{\isacharunderscore}duplicates\ {\isacharcolon}\isanewline
+\ \ \ \ {\isacharprime}a\ equal\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\isanewline
+end\ {\isacharequal}\ struct\isanewline
+\isanewline
+type\ {\isacharprime}a\ equal\ {\isacharequal}\ {\isacharbraceleft}equal\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ bool{\isacharbraceright}{\isacharsemicolon}\isanewline
+val\ equal\ {\isacharequal}\ {\isacharhash}equal\ {\isacharcolon}\ {\isacharprime}a\ equal\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ bool{\isacharsemicolon}\isanewline
+\isanewline
+fun\ eq\ A{\isacharunderscore}\ a\ b\ {\isacharequal}\ equal\ A{\isacharunderscore}\ a\ b{\isacharsemicolon}\isanewline
+\isanewline
+fun\ member\ A{\isacharunderscore}\ {\isacharbrackleft}{\isacharbrackright}\ y\ {\isacharequal}\ false\isanewline
+\ \ {\isacharbar}\ member\ A{\isacharunderscore}\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharparenright}\ y\ {\isacharequal}\ eq\ A{\isacharunderscore}\ x\ y\ orelse\ member\ A{\isacharunderscore}\ xs\ y{\isacharsemicolon}\isanewline
+\isanewline
+fun\ collect{\isacharunderscore}duplicates\ A{\isacharunderscore}\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs\isanewline
+\ \ {\isacharbar}\ collect{\isacharunderscore}duplicates\ A{\isacharunderscore}\ xs\ ys\ {\isacharparenleft}z\ {\isacharcolon}{\isacharcolon}\ zs{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ {\isacharparenleft}if\ member\ A{\isacharunderscore}\ xs\ z\isanewline
+\ \ \ \ \ \ then\ {\isacharparenleft}if\ member\ A{\isacharunderscore}\ ys\ z\ then\ collect{\isacharunderscore}duplicates\ A{\isacharunderscore}\ xs\ ys\ zs\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ A{\isacharunderscore}\ xs\ {\isacharparenleft}z\ {\isacharcolon}{\isacharcolon}\ ys{\isacharparenright}\ zs{\isacharparenright}\isanewline
+\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ A{\isacharunderscore}\ {\isacharparenleft}z\ {\isacharcolon}{\isacharcolon}\ xs{\isacharparenright}\ {\isacharparenleft}z\ {\isacharcolon}{\isacharcolon}\ ys{\isacharparenright}\ zs{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline
+
+  \end{typewriter}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -442,14 +443,14 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
-\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
-\hspace*{0pt} ~let {\char123}\\
-\hspace*{0pt} ~~~(y :~ys) = reverse xs;\\
-\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
-\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
+\begin{typewriter}
+    strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline
+strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ let\ {\isacharbraceleft}\isanewline
+\ \ \ \ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}\ {\isacharequal}\ reverse\ xs{\isacharsemicolon}\isanewline
+\ \ {\isacharbraceright}\ in\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharsemicolon}\isanewline
+strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isacharsemicolon}
+  \end{typewriter}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -533,16 +534,16 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\
-\hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
-\hspace*{0pt}\\
-\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
-\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
-\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
-\hspace*{0pt} ~(if null xs then empty{\char95}queue\\
-\hspace*{0pt} ~~~else strict{\char95}dequeue (AQueue [] (reverse xs)));%
+\begin{typewriter}
+    empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ a{\isacharsemicolon}\isanewline
+empty{\isacharunderscore}queue\ {\isacharequal}\ error\ {\isachardoublequote}empty{\isacharunderscore}queue{\isachardoublequote}{\isacharsemicolon}\isanewline
+\isanewline
+strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline
+strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isacharsemicolon}\isanewline
+strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ {\isacharparenleft}if\ null\ xs\ then\ empty{\isacharunderscore}queue\isanewline
+\ \ \ \ else\ strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}reverse\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}
+  \end{typewriter}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %

--- a/doc-src/Codegen/Thy/document/Further.tex	Thu Sep 23 17:22:45 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex	Thu Sep 23 21:17:11 2010 +0200
@@ -214,15 +214,15 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}funpow ::~forall a.~Nat -> (a -> a) -> a -> a;\\
-\hspace*{0pt}funpow Zero{\char95}nat f = id;\\
-\hspace*{0pt}funpow (Suc n) f = f .~funpow n f;\\
-\hspace*{0pt}\\
-\hspace*{0pt}funpows ::~forall a.~[Nat] -> (a -> a) -> a -> a;\\
-\hspace*{0pt}funpows [] = id;\\
-\hspace*{0pt}funpows (x :~xs) = funpow x .~funpows xs;%
+\begin{typewriter}
+    funpow\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Nat\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a\ {\isacharminus}{\isachargreater}\ a{\isacharparenright}\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
+funpow\ Zero{\isacharunderscore}nat\ f\ {\isacharequal}\ id{\isacharsemicolon}\isanewline
+funpow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ f\ {\isacharequal}\ f\ {\isachardot}\ funpow\ n\ f{\isacharsemicolon}\isanewline
+\isanewline
+funpows\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharbrackleft}Nat{\isacharbrackright}\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a\ {\isacharminus}{\isachargreater}\ a{\isacharparenright}\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
+funpows\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ id{\isacharsemicolon}\isanewline
+funpows\ {\isacharparenleft}x\ {\isacharcolon}\ xs{\isacharparenright}\ {\isacharequal}\ funpow\ x\ {\isachardot}\ funpows\ xs{\isacharsemicolon}
+  \end{typewriter}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %

--- a/doc-src/Codegen/Thy/document/Introduction.tex	Thu Sep 23 17:22:45 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex	Thu Sep 23 21:17:11 2010 +0200
@@ -140,41 +140,42 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt} ~val id :~'a -> 'a\\
-\hspace*{0pt} ~val fold :~('a -> 'b -> 'b) -> 'a list -> 'b -> 'b\\
-\hspace*{0pt} ~val rev :~'a list -> 'a list\\
-\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
-\hspace*{0pt} ~val empty :~'a queue\\
-\hspace*{0pt} ~val dequeue :~'a queue -> 'a option * 'a queue\\
-\hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
-\hspace*{0pt}end = struct\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun id x = (fn xa => xa) x;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun fold f [] = id\\
-\hspace*{0pt} ~| fold f (x ::~xs) = fold f xs o f x;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun rev xs = fold (fn a => fn b => a ::~b) xs [];\\
-\hspace*{0pt}\\
-\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
-\hspace*{0pt}\\
-\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun dequeue (AQueue ([],~[])) = (NONE,~AQueue ([],~[]))\\
-\hspace*{0pt} ~| dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
-\hspace*{0pt} ~| dequeue (AQueue (v ::~va,~[])) =\\
-\hspace*{0pt} ~~~let\\
-\hspace*{0pt} ~~~~~val y ::~ys = rev (v ::~va);\\
-\hspace*{0pt} ~~~in\\
-\hspace*{0pt} ~~~~~(SOME y,~AQueue ([],~ys))\\
-\hspace*{0pt} ~~~end;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
-\hspace*{0pt}\\
-\hspace*{0pt}end;~(*struct Example*)%
+\begin{typewriter}
+    structure\ Example\ {\isacharcolon}\ sig\isanewline
+\ \ val\ id\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
+\ \ val\ fold\ {\isacharcolon}\ {\isacharparenleft}{\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b{\isacharparenright}\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\isanewline
+\ \ val\ rev\ {\isacharcolon}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\isanewline
+\ \ datatype\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ of\ {\isacharprime}a\ list\ {\isacharasterisk}\ {\isacharprime}a\ list\isanewline
+\ \ val\ empty\ {\isacharcolon}\ {\isacharprime}a\ queue\isanewline
+\ \ val\ dequeue\ {\isacharcolon}\ {\isacharprime}a\ queue\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ option\ {\isacharasterisk}\ {\isacharprime}a\ queue\isanewline
+\ \ val\ enqueue\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ queue\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ queue\isanewline
+end\ {\isacharequal}\ struct\isanewline
+\isanewline
+fun\ id\ x\ {\isacharequal}\ {\isacharparenleft}fn\ xa\ {\isacharequal}{\isachargreater}\ xa{\isacharparenright}\ x{\isacharsemicolon}\isanewline
+\isanewline
+fun\ fold\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ id\isanewline
+\ \ {\isacharbar}\ fold\ f\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharparenright}\ {\isacharequal}\ fold\ f\ xs\ o\ f\ x{\isacharsemicolon}\isanewline
+\isanewline
+fun\ rev\ xs\ {\isacharequal}\ fold\ {\isacharparenleft}fn\ a\ {\isacharequal}{\isachargreater}\ fn\ b\ {\isacharequal}{\isachargreater}\ a\ {\isacharcolon}{\isacharcolon}\ b{\isacharparenright}\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline
+\isanewline
+datatype\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ of\ {\isacharprime}a\ list\ {\isacharasterisk}\ {\isacharprime}a\ list{\isacharsemicolon}\isanewline
+\isanewline
+val\ empty\ {\isacharcolon}\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+fun\ dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}NONE{\isacharcomma}\ AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
+\ \ {\isacharbar}\ dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}xs{\isacharcomma}\ y\ {\isacharcolon}{\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}SOME\ y{\isacharcomma}\ AQueue\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isacharparenright}\isanewline
+\ \ {\isacharbar}\ dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}v\ {\isacharcolon}{\isacharcolon}\ va{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ let\isanewline
+\ \ \ \ \ \ val\ y\ {\isacharcolon}{\isacharcolon}\ ys\ {\isacharequal}\ rev\ {\isacharparenleft}v\ {\isacharcolon}{\isacharcolon}\ va{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ \ \ in\isanewline
+\ \ \ \ \ \ {\isacharparenleft}SOME\ y{\isacharcomma}\ AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ ys{\isacharparenright}{\isacharparenright}\isanewline
+\ \ \ \ end{\isacharsemicolon}\isanewline
+\isanewline
+fun\ enqueue\ x\ {\isacharparenleft}AQueue\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharcomma}\ ys{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline
+
+  \end{typewriter}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -225,27 +226,28 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}module Example where {\char123}\\
-\hspace*{0pt}\\
-\hspace*{0pt}data Queue a = AQueue [a] [a];\\
-\hspace*{0pt}\\
-\hspace*{0pt}empty ::~forall a.~Queue a;\\
-\hspace*{0pt}empty = AQueue [] [];\\
-\hspace*{0pt}\\
-\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
-\hspace*{0pt}dequeue (AQueue [] []) = (Nothing,~AQueue [] []);\\
-\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
-\hspace*{0pt}dequeue (AQueue (v :~va) []) =\\
-\hspace*{0pt} ~let {\char123}\\
-\hspace*{0pt} ~~~(y :~ys) = reverse (v :~va);\\
-\hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys);\\
-\hspace*{0pt}\\
-\hspace*{0pt}enqueue ::~forall a.~a -> Queue a -> Queue a;\\
-\hspace*{0pt}enqueue x (AQueue xs ys) = AQueue (x :~xs) ys;\\
-\hspace*{0pt}\\
-\hspace*{0pt}{\char125}%
+\begin{typewriter}
+    module\ Example\ where\ {\isacharbraceleft}\isanewline
+\isanewline
+data\ Queue\ a\ {\isacharequal}\ AQueue\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharbrackleft}a{\isacharbrackright}{\isacharsemicolon}\isanewline
+\isanewline
+empty\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a{\isacharsemicolon}\isanewline
+empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline
+\isanewline
+dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Maybe\ a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline
+dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Nothing{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharsemicolon}\isanewline
+dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Just\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isacharsemicolon}\isanewline
+dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}v\ {\isacharcolon}\ va{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ let\ {\isacharbraceleft}\isanewline
+\ \ \ \ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}\ {\isacharequal}\ reverse\ {\isacharparenleft}v\ {\isacharcolon}\ va{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ {\isacharbraceright}\ in\ {\isacharparenleft}Just\ y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+enqueue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ a\ {\isacharminus}{\isachargreater}\ Queue\ a\ {\isacharminus}{\isachargreater}\ Queue\ a{\isacharsemicolon}\isanewline
+enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharcolon}\ xs{\isacharparenright}\ ys{\isacharsemicolon}\isanewline
+\isanewline
+{\isacharbraceright}\isanewline
+
+  \end{typewriter}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -393,47 +395,48 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}module Example where {\char123}\\
-\hspace*{0pt}\\
-\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\
-\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\
-\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\
-\hspace*{0pt}\\
-\hspace*{0pt}class Semigroup a where {\char123}\\
-\hspace*{0pt} ~mult ::~a -> a -> a;\\
-\hspace*{0pt}{\char125};\\
-\hspace*{0pt}\\
-\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\
-\hspace*{0pt} ~neutral ::~a;\\
-\hspace*{0pt}{\char125};\\
-\hspace*{0pt}\\
-\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\
-\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\
-\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\
-\hspace*{0pt}\\
-\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\
-\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\
-\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
-\hspace*{0pt}\\
-\hspace*{0pt}instance Semigroup Nat where {\char123}\\
-\hspace*{0pt} ~mult = mult{\char95}nat;\\
-\hspace*{0pt}{\char125};\\
-\hspace*{0pt}\\
-\hspace*{0pt}neutral{\char95}nat ::~Nat;\\
-\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}instance Monoid Nat where {\char123}\\
-\hspace*{0pt} ~neutral = neutral{\char95}nat;\\
-\hspace*{0pt}{\char125};\\
-\hspace*{0pt}\\
-\hspace*{0pt}bexp ::~Nat -> Nat;\\
-\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\
-\hspace*{0pt}\\
-\hspace*{0pt}{\char125}%
+\begin{typewriter}
+    module\ Example\ where\ {\isacharbraceleft}\isanewline
+\isanewline
+data\ Nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ Nat{\isacharsemicolon}\isanewline
+\isanewline
+plus{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
+plus{\isacharunderscore}nat\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n\ {\isacharequal}\ plus{\isacharunderscore}nat\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharsemicolon}\isanewline
+plus{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ n\ {\isacharequal}\ n{\isacharsemicolon}\isanewline
+\isanewline
+class\ Semigroup\ a\ where\ {\isacharbraceleft}\isanewline
+\ \ mult\ {\isacharcolon}{\isacharcolon}\ a\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
+{\isacharbraceright}{\isacharsemicolon}\isanewline
+\isanewline
+class\ {\isacharparenleft}Semigroup\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Monoid\ a\ where\ {\isacharbraceleft}\isanewline
+\ \ neutral\ {\isacharcolon}{\isacharcolon}\ a{\isacharsemicolon}\isanewline
+{\isacharbraceright}{\isacharsemicolon}\isanewline
+\isanewline
+pow\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Monoid\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Nat\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
+pow\ Zero{\isacharunderscore}nat\ a\ {\isacharequal}\ neutral{\isacharsemicolon}\isanewline
+pow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ mult\ a\ {\isacharparenleft}pow\ n\ a{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+mult{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
+mult{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ n\ {\isacharequal}\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline
+mult{\isacharunderscore}nat\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n\ {\isacharequal}\ plus{\isacharunderscore}nat\ n\ {\isacharparenleft}mult{\isacharunderscore}nat\ m\ n{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+instance\ Semigroup\ Nat\ where\ {\isacharbraceleft}\isanewline
+\ \ mult\ {\isacharequal}\ mult{\isacharunderscore}nat{\isacharsemicolon}\isanewline
+{\isacharbraceright}{\isacharsemicolon}\isanewline
+\isanewline
+neutral{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ Nat{\isacharsemicolon}\isanewline
+neutral{\isacharunderscore}nat\ {\isacharequal}\ Suc\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline
+\isanewline
+instance\ Monoid\ Nat\ where\ {\isacharbraceleft}\isanewline
+\ \ neutral\ {\isacharequal}\ neutral{\isacharunderscore}nat{\isacharsemicolon}\isanewline
+{\isacharbraceright}{\isacharsemicolon}\isanewline
+\isanewline
+bexp\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
+bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ Zero{\isacharunderscore}nat{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+{\isacharbraceright}\isanewline
+
+  \end{typewriter}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -458,52 +461,53 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
-\hspace*{0pt} ~val plus{\char95}nat :~nat -> nat -> nat\\
-\hspace*{0pt} ~type 'a semigroup\\
-\hspace*{0pt} ~val mult :~'a semigroup -> 'a -> 'a -> 'a\\
-\hspace*{0pt} ~type 'a monoid\\
-\hspace*{0pt} ~val semigroup{\char95}monoid :~'a monoid -> 'a semigroup\\
-\hspace*{0pt} ~val neutral :~'a monoid -> 'a\\
-\hspace*{0pt} ~val pow :~'a monoid -> nat -> 'a -> 'a\\
-\hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\
-\hspace*{0pt} ~val semigroup{\char95}nat :~nat semigroup\\
-\hspace*{0pt} ~val neutral{\char95}nat :~nat\\
-\hspace*{0pt} ~val monoid{\char95}nat :~nat monoid\\
-\hspace*{0pt} ~val bexp :~nat -> nat\\
-\hspace*{0pt}end = struct\\
-\hspace*{0pt}\\
-\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\
-\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
-\hspace*{0pt}\\
-\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
-\hspace*{0pt}val mult = {\char35}mult :~'a semigroup -> 'a -> 'a -> 'a;\\
-\hspace*{0pt}\\
-\hspace*{0pt}type 'a monoid = {\char123}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\
-\hspace*{0pt}val semigroup{\char95}monoid = {\char35}semigroup{\char95}monoid :~'a monoid -> 'a semigroup;\\
-\hspace*{0pt}val neutral = {\char35}neutral :~'a monoid -> 'a;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\
-\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\
-\hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
-\hspace*{0pt}\\
-\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\
-\hspace*{0pt}\\
-\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\
-\hspace*{0pt} ~:~nat monoid;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\
-\hspace*{0pt}\\
-\hspace*{0pt}end;~(*struct Example*)%
+\begin{typewriter}
+    structure\ Example\ {\isacharcolon}\ sig\isanewline
+\ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline
+\ \ val\ plus{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ nat\isanewline
+\ \ type\ {\isacharprime}a\ semigroup\isanewline
+\ \ val\ mult\ {\isacharcolon}\ {\isacharprime}a\ semigroup\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
+\ \ type\ {\isacharprime}a\ monoid\isanewline
+\ \ val\ semigroup{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ semigroup\isanewline
+\ \ val\ neutral\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
+\ \ val\ pow\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
+\ \ val\ mult{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ nat\isanewline
+\ \ val\ semigroup{\isacharunderscore}nat\ {\isacharcolon}\ nat\ semigroup\isanewline
+\ \ val\ neutral{\isacharunderscore}nat\ {\isacharcolon}\ nat\isanewline
+\ \ val\ monoid{\isacharunderscore}nat\ {\isacharcolon}\ nat\ monoid\isanewline
+\ \ val\ bexp\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\isanewline
+end\ {\isacharequal}\ struct\isanewline
+\isanewline
+datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat{\isacharsemicolon}\isanewline
+\isanewline
+fun\ plus{\isacharunderscore}nat\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n\ {\isacharequal}\ plus{\isacharunderscore}nat\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}\isanewline
+\ \ {\isacharbar}\ plus{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ n\ {\isacharequal}\ n{\isacharsemicolon}\isanewline
+\isanewline
+type\ {\isacharprime}a\ semigroup\ {\isacharequal}\ {\isacharbraceleft}mult\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharbraceright}{\isacharsemicolon}\isanewline
+val\ mult\ {\isacharequal}\ {\isacharhash}mult\ {\isacharcolon}\ {\isacharprime}a\ semigroup\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharsemicolon}\isanewline
+\isanewline
+type\ {\isacharprime}a\ monoid\ {\isacharequal}\ {\isacharbraceleft}semigroup{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ semigroup{\isacharcomma}\ neutral\ {\isacharcolon}\ {\isacharprime}a{\isacharbraceright}{\isacharsemicolon}\isanewline
+val\ semigroup{\isacharunderscore}monoid\ {\isacharequal}\ {\isacharhash}semigroup{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ semigroup{\isacharsemicolon}\isanewline
+val\ neutral\ {\isacharequal}\ {\isacharhash}neutral\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharsemicolon}\isanewline
+\isanewline
+fun\ pow\ A{\isacharunderscore}\ Zero{\isacharunderscore}nat\ a\ {\isacharequal}\ neutral\ A{\isacharunderscore}\isanewline
+\ \ {\isacharbar}\ pow\ A{\isacharunderscore}\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ mult\ {\isacharparenleft}semigroup{\isacharunderscore}monoid\ A{\isacharunderscore}{\isacharparenright}\ a\ {\isacharparenleft}pow\ A{\isacharunderscore}\ n\ a{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+fun\ mult{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ n\ {\isacharequal}\ Zero{\isacharunderscore}nat\isanewline
+\ \ {\isacharbar}\ mult{\isacharunderscore}nat\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n\ {\isacharequal}\ plus{\isacharunderscore}nat\ n\ {\isacharparenleft}mult{\isacharunderscore}nat\ m\ n{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+val\ semigroup{\isacharunderscore}nat\ {\isacharequal}\ {\isacharbraceleft}mult\ {\isacharequal}\ mult{\isacharunderscore}nat{\isacharbraceright}\ {\isacharcolon}\ nat\ semigroup{\isacharsemicolon}\isanewline
+\isanewline
+val\ neutral{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharequal}\ Suc\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline
+\isanewline
+val\ monoid{\isacharunderscore}nat\ {\isacharequal}\ {\isacharbraceleft}semigroup{\isacharunderscore}monoid\ {\isacharequal}\ semigroup{\isacharunderscore}nat{\isacharcomma}\ neutral\ {\isacharequal}\ neutral{\isacharunderscore}nat{\isacharbraceright}\isanewline
+\ \ {\isacharcolon}\ nat\ monoid{\isacharsemicolon}\isanewline
+\isanewline
+fun\ bexp\ n\ {\isacharequal}\ pow\ monoid{\isacharunderscore}nat\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ Zero{\isacharunderscore}nat{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline
+
+  \end{typewriter}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %

--- a/doc-src/Codegen/Thy/document/Refinement.tex	Thu Sep 23 17:22:45 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Refinement.tex	Thu Sep 23 21:17:11 2010 +0200
@@ -72,12 +72,12 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}fib ::~Nat -> Nat;\\
-\hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;\\
-\hspace*{0pt}fib (Suc Zero{\char95}nat) = Suc Zero{\char95}nat;\\
-\hspace*{0pt}fib (Suc (Suc n)) = plus{\char95}nat (fib n) (fib (Suc n));%
+\begin{typewriter}
+    fib\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
+fib\ Zero{\isacharunderscore}nat\ {\isacharequal}\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline
+fib\ {\isacharparenleft}Suc\ Zero{\isacharunderscore}nat{\isacharparenright}\ {\isacharequal}\ Suc\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline
+fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ plus{\isacharunderscore}nat\ {\isacharparenleft}fib\ n{\isacharparenright}\ {\isacharparenleft}fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isacharsemicolon}
+  \end{typewriter}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -170,17 +170,17 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}fib{\char95}step ::~Nat -> (Nat,~Nat);\\
-\hspace*{0pt}fib{\char95}step (Suc n) = let {\char123}\\
-\hspace*{0pt} ~~~~~~~~~~~~~~~~~~~~(m,~q) = fib{\char95}step n;\\
-\hspace*{0pt} ~~~~~~~~~~~~~~~~~~{\char125}~in (plus{\char95}nat m q,~m);\\
-\hspace*{0pt}fib{\char95}step Zero{\char95}nat = (Suc Zero{\char95}nat,~Zero{\char95}nat);\\
-\hspace*{0pt}\\
-\hspace*{0pt}fib ::~Nat -> Nat;\\
-\hspace*{0pt}fib (Suc n) = fst (fib{\char95}step n);\\
-\hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;%
+\begin{typewriter}
+    fib{\isacharunderscore}step\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Nat{\isacharcomma}\ Nat{\isacharparenright}{\isacharsemicolon}\isanewline
+fib{\isacharunderscore}step\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ let\ {\isacharbraceleft}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}m{\isacharcomma}\ q{\isacharparenright}\ {\isacharequal}\ fib{\isacharunderscore}step\ n{\isacharsemicolon}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbraceright}\ in\ {\isacharparenleft}plus{\isacharunderscore}nat\ m\ q{\isacharcomma}\ m{\isacharparenright}{\isacharsemicolon}\isanewline
+fib{\isacharunderscore}step\ Zero{\isacharunderscore}nat\ {\isacharequal}\ {\isacharparenleft}Suc\ Zero{\isacharunderscore}nat{\isacharcomma}\ Zero{\isacharunderscore}nat{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+fib\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
+fib\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ fst\ {\isacharparenleft}fib{\isacharunderscore}step\ n{\isacharparenright}{\isacharsemicolon}\isanewline
+fib\ Zero{\isacharunderscore}nat\ {\isacharequal}\ Zero{\isacharunderscore}nat{\isacharsemicolon}
+  \end{typewriter}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -348,41 +348,42 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt} ~val id :~'a -> 'a\\
-\hspace*{0pt} ~val fold :~('a -> 'b -> 'b) -> 'a list -> 'b -> 'b\\
-\hspace*{0pt} ~val rev :~'a list -> 'a list\\
-\hspace*{0pt} ~val null :~'a list -> bool\\
-\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
-\hspace*{0pt} ~val empty :~'a queue\\
-\hspace*{0pt} ~val dequeue :~'a queue -> 'a option * 'a queue\\
-\hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
-\hspace*{0pt}end = struct\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun id x = (fn xa => xa) x;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun fold f [] = id\\
-\hspace*{0pt} ~| fold f (x ::~xs) = fold f xs o f x;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun rev xs = fold (fn a => fn b => a ::~b) xs [];\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun null [] = true\\
-\hspace*{0pt} ~| null (x ::~xs) = false;\\
-\hspace*{0pt}\\
-\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
-\hspace*{0pt}\\
-\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
-\hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\
-\hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\
-\hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
-\hspace*{0pt}\\
-\hspace*{0pt}end;~(*struct Example*)%
+\begin{typewriter}
+    structure\ Example\ {\isacharcolon}\ sig\isanewline
+\ \ val\ id\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
+\ \ val\ fold\ {\isacharcolon}\ {\isacharparenleft}{\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b{\isacharparenright}\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\isanewline
+\ \ val\ rev\ {\isacharcolon}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\isanewline
+\ \ val\ null\ {\isacharcolon}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ bool\isanewline
+\ \ datatype\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ of\ {\isacharprime}a\ list\ {\isacharasterisk}\ {\isacharprime}a\ list\isanewline
+\ \ val\ empty\ {\isacharcolon}\ {\isacharprime}a\ queue\isanewline
+\ \ val\ dequeue\ {\isacharcolon}\ {\isacharprime}a\ queue\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ option\ {\isacharasterisk}\ {\isacharprime}a\ queue\isanewline
+\ \ val\ enqueue\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ queue\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ queue\isanewline
+end\ {\isacharequal}\ struct\isanewline
+\isanewline
+fun\ id\ x\ {\isacharequal}\ {\isacharparenleft}fn\ xa\ {\isacharequal}{\isachargreater}\ xa{\isacharparenright}\ x{\isacharsemicolon}\isanewline
+\isanewline
+fun\ fold\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ id\isanewline
+\ \ {\isacharbar}\ fold\ f\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharparenright}\ {\isacharequal}\ fold\ f\ xs\ o\ f\ x{\isacharsemicolon}\isanewline
+\isanewline
+fun\ rev\ xs\ {\isacharequal}\ fold\ {\isacharparenleft}fn\ a\ {\isacharequal}{\isachargreater}\ fn\ b\ {\isacharequal}{\isachargreater}\ a\ {\isacharcolon}{\isacharcolon}\ b{\isacharparenright}\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline
+\isanewline
+fun\ null\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ true\isanewline
+\ \ {\isacharbar}\ null\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharparenright}\ {\isacharequal}\ false{\isacharsemicolon}\isanewline
+\isanewline
+datatype\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ of\ {\isacharprime}a\ list\ {\isacharasterisk}\ {\isacharprime}a\ list{\isacharsemicolon}\isanewline
+\isanewline
+val\ empty\ {\isacharcolon}\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+fun\ dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}xs{\isacharcomma}\ y\ {\isacharcolon}{\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}SOME\ y{\isacharcomma}\ AQueue\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isacharparenright}\isanewline
+\ \ {\isacharbar}\ dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}xs{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ {\isacharparenleft}if\ null\ xs\ then\ {\isacharparenleft}NONE{\isacharcomma}\ AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
+\ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+fun\ enqueue\ x\ {\isacharparenleft}AQueue\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharcomma}\ ys{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline
+
+  \end{typewriter}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -584,36 +585,37 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}module Example where {\char123}\\
-\hspace*{0pt}\\
-\hspace*{0pt}newtype Dlist a = Dlist [a];\\
-\hspace*{0pt}\\
-\hspace*{0pt}empty ::~forall a.~Dlist a;\\
-\hspace*{0pt}empty = Dlist [];\\
-\hspace*{0pt}\\
-\hspace*{0pt}member ::~forall a.~(Eq a) => [a] -> a -> Bool;\\
-\hspace*{0pt}member [] y = False;\\
-\hspace*{0pt}member (x :~xs) y = x == y || member xs y;\\
-\hspace*{0pt}\\
-\hspace*{0pt}insert ::~forall a.~(Eq a) => a -> [a] -> [a];\\
-\hspace*{0pt}insert x xs = (if member xs x then xs else x :~xs);\\
-\hspace*{0pt}\\
-\hspace*{0pt}list{\char95}of{\char95}dlist ::~forall a.~Dlist a -> [a];\\
-\hspace*{0pt}list{\char95}of{\char95}dlist (Dlist x) = x;\\
-\hspace*{0pt}\\
-\hspace*{0pt}inserta ::~forall a.~(Eq a) => a -> Dlist a -> Dlist a;\\
-\hspace*{0pt}inserta x dxs = Dlist (insert x (list{\char95}of{\char95}dlist dxs));\\
-\hspace*{0pt}\\
-\hspace*{0pt}remove1 ::~forall a.~(Eq a) => a -> [a] -> [a];\\
-\hspace*{0pt}remove1 x [] = [];\\
-\hspace*{0pt}remove1 x (y :~xs) = (if x == y then xs else y :~remove1 x xs);\\
-\hspace*{0pt}\\
-\hspace*{0pt}remove ::~forall a.~(Eq a) => a -> Dlist a -> Dlist a;\\
-\hspace*{0pt}remove x dxs = Dlist (remove1 x (list{\char95}of{\char95}dlist dxs));\\
-\hspace*{0pt}\\
-\hspace*{0pt}{\char125}%
+\begin{typewriter}
+    module\ Example\ where\ {\isacharbraceleft}\isanewline
+\isanewline
+newtype\ Dlist\ a\ {\isacharequal}\ Dlist\ {\isacharbrackleft}a{\isacharbrackright}{\isacharsemicolon}\isanewline
+\isanewline
+empty\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Dlist\ a{\isacharsemicolon}\isanewline
+empty\ {\isacharequal}\ Dlist\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline
+\isanewline
+member\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Eq\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ Bool{\isacharsemicolon}\isanewline
+member\ {\isacharbrackleft}{\isacharbrackright}\ y\ {\isacharequal}\ False{\isacharsemicolon}\isanewline
+member\ {\isacharparenleft}x\ {\isacharcolon}\ xs{\isacharparenright}\ y\ {\isacharequal}\ x\ {\isacharequal}{\isacharequal}\ y\ {\isacharbar}{\isacharbar}\ member\ xs\ y{\isacharsemicolon}\isanewline
+\isanewline
+insert\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Eq\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharminus}{\isachargreater}\ {\isacharbrackleft}a{\isacharbrackright}{\isacharsemicolon}\isanewline
+insert\ x\ xs\ {\isacharequal}\ {\isacharparenleft}if\ member\ xs\ x\ then\ xs\ else\ x\ {\isacharcolon}\ xs{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+list{\isacharunderscore}of{\isacharunderscore}dlist\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Dlist\ a\ {\isacharminus}{\isachargreater}\ {\isacharbrackleft}a{\isacharbrackright}{\isacharsemicolon}\isanewline
+list{\isacharunderscore}of{\isacharunderscore}dlist\ {\isacharparenleft}Dlist\ x{\isacharparenright}\ {\isacharequal}\ x{\isacharsemicolon}\isanewline
+\isanewline
+inserta\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Eq\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ Dlist\ a\ {\isacharminus}{\isachargreater}\ Dlist\ a{\isacharsemicolon}\isanewline
+inserta\ x\ dxs\ {\isacharequal}\ Dlist\ {\isacharparenleft}insert\ x\ {\isacharparenleft}list{\isacharunderscore}of{\isacharunderscore}dlist\ dxs{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+remove{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Eq\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharminus}{\isachargreater}\ {\isacharbrackleft}a{\isacharbrackright}{\isacharsemicolon}\isanewline
+remove{\isadigit{1}}\ x\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline
+remove{\isadigit{1}}\ x\ {\isacharparenleft}y\ {\isacharcolon}\ xs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isacharequal}{\isacharequal}\ y\ then\ xs\ else\ y\ {\isacharcolon}\ remove{\isadigit{1}}\ x\ xs{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+remove\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Eq\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ Dlist\ a\ {\isacharminus}{\isachargreater}\ Dlist\ a{\isacharsemicolon}\isanewline
+remove\ x\ dxs\ {\isacharequal}\ Dlist\ {\isacharparenleft}remove{\isadigit{1}}\ x\ {\isacharparenleft}list{\isacharunderscore}of{\isacharunderscore}dlist\ dxs{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+{\isacharbraceright}\isanewline
+
+  \end{typewriter}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %

--- a/doc-src/Codegen/style.sty	Thu Sep 23 17:22:45 2010 +0200
+++ b/doc-src/Codegen/style.sty	Thu Sep 23 21:17:11 2010 +0200
@@ -8,6 +8,7 @@
 
 %% references
 \newcommand{\secref}[1]{\S\ref{#1}}
+\newcommand{\figref}[1]{figure~\ref{#1}}
 
 %% logical markup
 \newcommand{\strong}[1]{{\bfseries {#1}}}
@@ -26,9 +27,15 @@
 \renewcommand{\endisatagquote}{\end{quote}}
 \newcommand{\quotebreak}{\\[1.2ex]}
 
+%% typewriter text
+\newenvironment{typewriter}{\renewcommand{\isadigit}[1]{{##1}}%
+\parindent0pt%
+\fontsize{9pt}{0pt}%
+\isabellestyle{tt}\isastyle}{}
+
 \isakeeptag{quotett}
 \renewcommand{\isatagquotett}{\begin{quote}\isabellestyle{tt}\isastyle}
-\renewcommand{\endisatagquotett}{\end{quote}\isabellestyle{it}\isastyle}
+\renewcommand{\endisatagquotett}{\end{quote}}
 
 %% a trick
 \newcommand{\isasymSML}{SML}

--- a/doc-src/isabelle.sty	Thu Sep 23 17:22:45 2010 +0200
+++ b/doc-src/isabelle.sty	Thu Sep 23 21:17:11 2010 +0200
@@ -46,8 +46,6 @@
 {\begin{trivlist}\begin{isabellebody}\item\relax}
 {\end{isabellebody}\end{trivlist}}
 
-\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
-
 \newcommand{\isa}[1]{\emph{\isastyleminor #1}}
 
 \newcommand{\isaindent}[1]{\hphantom{#1}}

--- a/lib/texinputs/isabelle.sty	Thu Sep 23 17:22:45 2010 +0200
+++ b/lib/texinputs/isabelle.sty	Thu Sep 23 21:17:11 2010 +0200
@@ -46,8 +46,6 @@
 {\begin{trivlist}\begin{isabellebody}\item\relax}
 {\end{isabellebody}\end{trivlist}}
 
-\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
-
 \newcommand{\isa}[1]{\emph{\isastyleminor #1}}
 
 \newcommand{\isaindent}[1]{\hphantom{#1}}

--- a/src/Pure/Thy/latex.ML	Thu Sep 23 17:22:45 2010 +0200
+++ b/src/Pure/Thy/latex.ML	Thu Sep 23 21:17:11 2010 +0200
@@ -13,7 +13,6 @@
   val output_markup: string -> string -> string
   val output_markup_env: string -> string -> string
   val output_verbatim: string -> string
-  val output_typewriter: string -> string
   val markup_true: string
   val markup_false: string
   val begin_delim: string -> string
@@ -98,38 +97,6 @@
 
 end;
 
-fun output_typewriter s =
-  let
-    val parse = Scan.repeat
-      (Scan.this_string "\n" |-- Scan.succeed "\\\\\n\\hspace*{0pt}"
-        || (Scan.this_string " "
-          || Scan.this_string "."
-          || Scan.this_string ","
-          || Scan.this_string ":"
-          || Scan.this_string ";"
-          || Scan.this_string "\"" |-- Scan.succeed "{\\char34}"
-          || Scan.this_string "#" |-- Scan.succeed "{\\char35}"
-          || Scan.this_string "$" |-- Scan.succeed "{\\char36}"
-          || Scan.this_string "%" |-- Scan.succeed "{\\char37}"
-          || Scan.this_string "&" |-- Scan.succeed "{\\char38}"
-          || Scan.this_string "\\" |-- Scan.succeed "{\\char92}"
-          || Scan.this_string "^" |-- Scan.succeed "{\\char94}"
-          || Scan.this_string "_" |-- Scan.succeed "{\\char95}"
-          || Scan.this_string "{" |-- Scan.succeed "{\\char123}"
-          || Scan.this_string "}" |-- Scan.succeed "{\\char125}"
-          || Scan.this_string "~" |-- Scan.succeed "{\\char126}")
-          -- Scan.repeat (Scan.this_string " ")
-          >> (fn (x, xs) => x ^ replicate_string (length xs) "~")
-        || Scan.one Symbol.not_eof);
-    fun is_newline s = (s = "\n");
-    val cs = explode s |> take_prefix is_newline |> snd
-      |> take_suffix is_newline |> fst;
-    val (texts, []) =  Scan.finite Symbol.stopper parse cs
-  in if null texts
-    then ""
-    else implode ("\\isatypewriter%\n\\noindent%\n\\hspace*{0pt}" :: texts)
-  end
-
 
 (* token output *)
 

--- a/src/Tools/Code/code_target.ML	Thu Sep 23 17:22:45 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Thu Sep 23 21:17:11 2010 +0200
@@ -73,9 +73,14 @@
 datatype destination = Export of Path.T option | Produce | Present of string list;
 type serialization = int -> destination -> (string * (string -> string option)) option;
 
-fun serialization output _ content width (Export some_path) = (output width some_path content; NONE)
-  | serialization _ string content width Produce = SOME (string [] width content)
-  | serialization _ string content width (Present stmt_names) = SOME (string stmt_names width content);
+fun serialization output _ content width (Export some_path) =
+      (output width some_path content; NONE)
+  | serialization _ string content width Produce =
+      string [] width content |> SOME
+  | serialization _ string content width (Present stmt_names) =
+     string stmt_names width content
+     |> apfst (Pretty.output (SOME width) o Pretty.str)
+     |> SOME;
 
 fun export some_path f = (f (Export some_path); ());
 fun produce f = the (f Produce);
@@ -475,7 +480,7 @@
       present_code thy (mk_cs thy)
         (fn naming => maps (fn f => f thy naming) mk_stmtss)
         target some_width "Example" []
-      |> Latex.output_typewriter
+      (*|> Latex.output_typewriter*)
     end);
 
 end;