more canonical type setting of type writer code examples
authorhaftmann
Thu Sep 23 15:46:17 2010 +0200 (2010-09-23)
changeset 396640afaf89ab591
parent 39663 5096018d5359
child 39665 f1622d126e31
more canonical type setting of type writer code examples
doc-src/Classes/Thy/Classes.thy
doc-src/Classes/Thy/document/Classes.tex
doc-src/Classes/style.sty
doc-src/Codegen/Thy/Adaptation.thy
doc-src/Codegen/Thy/Foundations.thy
doc-src/Codegen/Thy/Further.thy
doc-src/Codegen/Thy/Introduction.thy
doc-src/Codegen/Thy/Refinement.thy
doc-src/Codegen/Thy/document/Adaptation.tex
doc-src/Codegen/Thy/document/Foundations.tex
doc-src/Codegen/Thy/document/Further.tex
doc-src/Codegen/Thy/document/Introduction.tex
doc-src/Codegen/Thy/document/Refinement.tex
doc-src/Codegen/style.sty
     1.1 --- a/doc-src/Classes/Thy/Classes.thy	Thu Sep 23 13:28:53 2010 +0200
     1.2 +++ b/doc-src/Classes/Thy/Classes.thy	Thu Sep 23 15:46:17 2010 +0200
     1.3 @@ -601,18 +601,31 @@
     1.4    \noindent This maps to Haskell as follows:
     1.5  *}
     1.6  (*<*)code_include %invisible Haskell "Natural" -(*>*)
     1.7 -text %quote {*@{code_stmts example (Haskell)}*}
     1.8 +text %quote {*
     1.9 +  \begin{typewriter}
    1.10 +    @{code_stmts example (Haskell)}
    1.11 +  \end{typewriter}
    1.12 +*}
    1.13  
    1.14  text {*
    1.15    \noindent The code in SML has explicit dictionary passing:
    1.16  *}
    1.17 -text %quote {*@{code_stmts example (SML)}*}
    1.18 +text %quote {*
    1.19 +  \begin{typewriter}
    1.20 +    @{code_stmts example (SML)}
    1.21 +  \end{typewriter}
    1.22 +*}
    1.23 +
    1.24  
    1.25  text {*
    1.26    \noindent In Scala, implicts are used as dictionaries:
    1.27  *}
    1.28  (*<*)code_include %invisible Scala "Natural" -(*>*)
    1.29 -text %quote {*@{code_stmts example (Scala)}*}
    1.30 +text %quote {*
    1.31 +  \begin{typewriter}
    1.32 +    @{code_stmts example (Scala)}
    1.33 +  \end{typewriter}
    1.34 +*}
    1.35  
    1.36  
    1.37  subsection {* Inspecting the type class universe *}
     2.1 --- a/doc-src/Classes/Thy/document/Classes.tex	Thu Sep 23 13:28:53 2010 +0200
     2.2 +++ b/doc-src/Classes/Thy/document/Classes.tex	Thu Sep 23 15:46:17 2010 +0200
     2.3 @@ -1130,70 +1130,71 @@
     2.4  \isatagquote
     2.5  %
     2.6  \begin{isamarkuptext}%
     2.7 -\isatypewriter%
     2.8 -\noindent%
     2.9 -\hspace*{0pt}module Example where {\char123}\\
    2.10 -\hspace*{0pt}\\
    2.11 -\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
    2.12 -\hspace*{0pt}\\
    2.13 -\hspace*{0pt}nat{\char95}aux ::~Integer -> Nat -> Nat;\\
    2.14 -\hspace*{0pt}nat{\char95}aux i n = (if i <= 0 then n else nat{\char95}aux (i - 1) (Suc n));\\
    2.15 -\hspace*{0pt}\\
    2.16 -\hspace*{0pt}nat ::~Integer -> Nat;\\
    2.17 -\hspace*{0pt}nat i = nat{\char95}aux i Zero{\char95}nat;\\
    2.18 -\hspace*{0pt}\\
    2.19 -\hspace*{0pt}class Semigroup a where {\char123}\\
    2.20 -\hspace*{0pt} ~mult ::~a -> a -> a;\\
    2.21 -\hspace*{0pt}{\char125};\\
    2.22 -\hspace*{0pt}\\
    2.23 -\hspace*{0pt}class (Semigroup a) => Monoidl a where {\char123}\\
    2.24 -\hspace*{0pt} ~neutral ::~a;\\
    2.25 -\hspace*{0pt}{\char125};\\
    2.26 -\hspace*{0pt}\\
    2.27 -\hspace*{0pt}class (Monoidl a) => Monoid a where {\char123}\\
    2.28 -\hspace*{0pt}{\char125};\\
    2.29 -\hspace*{0pt}\\
    2.30 -\hspace*{0pt}class (Monoid a) => Group a where {\char123}\\
    2.31 -\hspace*{0pt} ~inverse ::~a -> a;\\
    2.32 -\hspace*{0pt}{\char125};\\
    2.33 -\hspace*{0pt}\\
    2.34 -\hspace*{0pt}pow{\char95}nat ::~forall a.~(Monoid a) => Nat -> a -> a;\\
    2.35 -\hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\
    2.36 -\hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\
    2.37 -\hspace*{0pt}\\
    2.38 -\hspace*{0pt}pow{\char95}int ::~forall a.~(Group a) => Integer -> a -> a;\\
    2.39 -\hspace*{0pt}pow{\char95}int k x =\\
    2.40 -\hspace*{0pt} ~(if 0 <= k then pow{\char95}nat (nat k) x\\
    2.41 -\hspace*{0pt} ~~~else inverse (pow{\char95}nat (nat (negate k)) x));\\
    2.42 -\hspace*{0pt}\\
    2.43 -\hspace*{0pt}mult{\char95}int ::~Integer -> Integer -> Integer;\\
    2.44 -\hspace*{0pt}mult{\char95}int i j = i + j;\\
    2.45 -\hspace*{0pt}\\
    2.46 -\hspace*{0pt}instance Semigroup Integer where {\char123}\\
    2.47 -\hspace*{0pt} ~mult = mult{\char95}int;\\
    2.48 -\hspace*{0pt}{\char125};\\
    2.49 -\hspace*{0pt}\\
    2.50 -\hspace*{0pt}neutral{\char95}int ::~Integer;\\
    2.51 -\hspace*{0pt}neutral{\char95}int = 0;\\
    2.52 -\hspace*{0pt}\\
    2.53 -\hspace*{0pt}instance Monoidl Integer where {\char123}\\
    2.54 -\hspace*{0pt} ~neutral = neutral{\char95}int;\\
    2.55 -\hspace*{0pt}{\char125};\\
    2.56 -\hspace*{0pt}\\
    2.57 -\hspace*{0pt}instance Monoid Integer where {\char123}\\
    2.58 -\hspace*{0pt}{\char125};\\
    2.59 -\hspace*{0pt}\\
    2.60 -\hspace*{0pt}inverse{\char95}int ::~Integer -> Integer;\\
    2.61 -\hspace*{0pt}inverse{\char95}int i = negate i;\\
    2.62 -\hspace*{0pt}\\
    2.63 -\hspace*{0pt}instance Group Integer where {\char123}\\
    2.64 -\hspace*{0pt} ~inverse = inverse{\char95}int;\\
    2.65 -\hspace*{0pt}{\char125};\\
    2.66 -\hspace*{0pt}\\
    2.67 -\hspace*{0pt}example ::~Integer;\\
    2.68 -\hspace*{0pt}example = pow{\char95}int 10 (-2);\\
    2.69 -\hspace*{0pt}\\
    2.70 -\hspace*{0pt}{\char125}%
    2.71 +\begin{typewriter}
    2.72 +    module\ Example\ where\ {\isacharbraceleft}\isanewline
    2.73 +\isanewline
    2.74 +data\ Nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ Nat{\isacharsemicolon}\isanewline
    2.75 +\isanewline
    2.76 +nat{\isacharunderscore}aux\ {\isacharcolon}{\isacharcolon}\ Integer\ {\isacharminus}{\isachargreater}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
    2.77 +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
    2.78 +\isanewline
    2.79 +nat\ {\isacharcolon}{\isacharcolon}\ Integer\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
    2.80 +nat\ i\ {\isacharequal}\ nat{\isacharunderscore}aux\ i\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline
    2.81 +\isanewline
    2.82 +class\ Semigroup\ a\ where\ {\isacharbraceleft}\isanewline
    2.83 +\ \ mult\ {\isacharcolon}{\isacharcolon}\ a\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
    2.84 +{\isacharbraceright}{\isacharsemicolon}\isanewline
    2.85 +\isanewline
    2.86 +class\ {\isacharparenleft}Semigroup\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Monoidl\ a\ where\ {\isacharbraceleft}\isanewline
    2.87 +\ \ neutral\ {\isacharcolon}{\isacharcolon}\ a{\isacharsemicolon}\isanewline
    2.88 +{\isacharbraceright}{\isacharsemicolon}\isanewline
    2.89 +\isanewline
    2.90 +class\ {\isacharparenleft}Monoidl\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Monoid\ a\ where\ {\isacharbraceleft}\isanewline
    2.91 +{\isacharbraceright}{\isacharsemicolon}\isanewline
    2.92 +\isanewline
    2.93 +class\ {\isacharparenleft}Monoid\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Group\ a\ where\ {\isacharbraceleft}\isanewline
    2.94 +\ \ inverse\ {\isacharcolon}{\isacharcolon}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
    2.95 +{\isacharbraceright}{\isacharsemicolon}\isanewline
    2.96 +\isanewline
    2.97 +pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Monoid\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Nat\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
    2.98 +pow{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ x\ {\isacharequal}\ neutral{\isacharsemicolon}\isanewline
    2.99 +pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ mult\ x\ {\isacharparenleft}pow{\isacharunderscore}nat\ n\ x{\isacharparenright}{\isacharsemicolon}\isanewline
   2.100 +\isanewline
   2.101 +pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Group\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Integer\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
   2.102 +pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\isanewline
   2.103 +\ \ {\isacharparenleft}if\ {\isadigit{0}}\ {\isacharless}{\isacharequal}\ k\ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
   2.104 +\ \ \ \ else\ inverse\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}negate\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
   2.105 +\isanewline
   2.106 +mult{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ Integer\ {\isacharminus}{\isachargreater}\ Integer\ {\isacharminus}{\isachargreater}\ Integer{\isacharsemicolon}\isanewline
   2.107 +mult{\isacharunderscore}int\ i\ j\ {\isacharequal}\ i\ {\isacharplus}\ j{\isacharsemicolon}\isanewline
   2.108 +\isanewline
   2.109 +instance\ Semigroup\ Integer\ where\ {\isacharbraceleft}\isanewline
   2.110 +\ \ mult\ {\isacharequal}\ mult{\isacharunderscore}int{\isacharsemicolon}\isanewline
   2.111 +{\isacharbraceright}{\isacharsemicolon}\isanewline
   2.112 +\isanewline
   2.113 +neutral{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ Integer{\isacharsemicolon}\isanewline
   2.114 +neutral{\isacharunderscore}int\ {\isacharequal}\ {\isadigit{0}}{\isacharsemicolon}\isanewline
   2.115 +\isanewline
   2.116 +instance\ Monoidl\ Integer\ where\ {\isacharbraceleft}\isanewline
   2.117 +\ \ neutral\ {\isacharequal}\ neutral{\isacharunderscore}int{\isacharsemicolon}\isanewline
   2.118 +{\isacharbraceright}{\isacharsemicolon}\isanewline
   2.119 +\isanewline
   2.120 +instance\ Monoid\ Integer\ where\ {\isacharbraceleft}\isanewline
   2.121 +{\isacharbraceright}{\isacharsemicolon}\isanewline
   2.122 +\isanewline
   2.123 +inverse{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ Integer\ {\isacharminus}{\isachargreater}\ Integer{\isacharsemicolon}\isanewline
   2.124 +inverse{\isacharunderscore}int\ i\ {\isacharequal}\ negate\ i{\isacharsemicolon}\isanewline
   2.125 +\isanewline
   2.126 +instance\ Group\ Integer\ where\ {\isacharbraceleft}\isanewline
   2.127 +\ \ inverse\ {\isacharequal}\ inverse{\isacharunderscore}int{\isacharsemicolon}\isanewline
   2.128 +{\isacharbraceright}{\isacharsemicolon}\isanewline
   2.129 +\isanewline
   2.130 +example\ {\isacharcolon}{\isacharcolon}\ Integer{\isacharsemicolon}\isanewline
   2.131 +example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isacharsemicolon}\isanewline
   2.132 +\isanewline
   2.133 +{\isacharbraceright}\isanewline
   2.134 +
   2.135 +  \end{typewriter}%
   2.136  \end{isamarkuptext}%
   2.137  \isamarkuptrue%
   2.138  %
   2.139 @@ -1216,86 +1217,87 @@
   2.140  \isatagquote
   2.141  %
   2.142  \begin{isamarkuptext}%
   2.143 -\isatypewriter%
   2.144 -\noindent%
   2.145 -\hspace*{0pt}structure Example :~sig\\
   2.146 -\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
   2.147 -\hspace*{0pt} ~val nat{\char95}aux :~IntInf.int -> nat -> nat\\
   2.148 -\hspace*{0pt} ~val nat :~IntInf.int -> nat\\
   2.149 -\hspace*{0pt} ~type 'a semigroup\\
   2.150 -\hspace*{0pt} ~val mult :~'a semigroup -> 'a -> 'a -> 'a\\
   2.151 -\hspace*{0pt} ~type 'a monoidl\\
   2.152 -\hspace*{0pt} ~val semigroup{\char95}monoidl :~'a monoidl -> 'a semigroup\\
   2.153 -\hspace*{0pt} ~val neutral :~'a monoidl -> 'a\\
   2.154 -\hspace*{0pt} ~type 'a monoid\\
   2.155 -\hspace*{0pt} ~val monoidl{\char95}monoid :~'a monoid -> 'a monoidl\\
   2.156 -\hspace*{0pt} ~type 'a group\\
   2.157 -\hspace*{0pt} ~val monoid{\char95}group :~'a group -> 'a monoid\\
   2.158 -\hspace*{0pt} ~val inverse :~'a group -> 'a -> 'a\\
   2.159 -\hspace*{0pt} ~val pow{\char95}nat :~'a monoid -> nat -> 'a -> 'a\\
   2.160 -\hspace*{0pt} ~val pow{\char95}int :~'a group -> IntInf.int -> 'a -> 'a\\
   2.161 -\hspace*{0pt} ~val mult{\char95}int :~IntInf.int -> IntInf.int -> IntInf.int\\
   2.162 -\hspace*{0pt} ~val semigroup{\char95}int :~IntInf.int semigroup\\
   2.163 -\hspace*{0pt} ~val neutral{\char95}int :~IntInf.int\\
   2.164 -\hspace*{0pt} ~val monoidl{\char95}int :~IntInf.int monoidl\\
   2.165 -\hspace*{0pt} ~val monoid{\char95}int :~IntInf.int monoid\\
   2.166 -\hspace*{0pt} ~val inverse{\char95}int :~IntInf.int -> IntInf.int\\
   2.167 -\hspace*{0pt} ~val group{\char95}int :~IntInf.int group\\
   2.168 -\hspace*{0pt} ~val example :~IntInf.int\\
   2.169 -\hspace*{0pt}end = struct\\
   2.170 -\hspace*{0pt}\\
   2.171 -\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
   2.172 -\hspace*{0pt}\\
   2.173 -\hspace*{0pt}fun nat{\char95}aux i n =\\
   2.174 -\hspace*{0pt} ~(if IntInf.<= (i,~(0 :~IntInf.int)) then n\\
   2.175 -\hspace*{0pt} ~~~else nat{\char95}aux (IntInf.- (i,~(1 :~IntInf.int))) (Suc n));\\
   2.176 -\hspace*{0pt}\\
   2.177 -\hspace*{0pt}fun nat i = nat{\char95}aux i Zero{\char95}nat;\\
   2.178 -\hspace*{0pt}\\
   2.179 -\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
   2.180 -\hspace*{0pt}val mult = {\char35}mult :~'a semigroup -> 'a -> 'a -> 'a;\\
   2.181 -\hspace*{0pt}\\
   2.182 -\hspace*{0pt}type 'a monoidl = {\char123}semigroup{\char95}monoidl :~'a semigroup,~neutral :~'a{\char125};\\
   2.183 -\hspace*{0pt}val semigroup{\char95}monoidl = {\char35}semigroup{\char95}monoidl :~'a monoidl -> 'a semigroup;\\
   2.184 -\hspace*{0pt}val neutral = {\char35}neutral :~'a monoidl -> 'a;\\
   2.185 -\hspace*{0pt}\\
   2.186 -\hspace*{0pt}type 'a monoid = {\char123}monoidl{\char95}monoid :~'a monoidl{\char125};\\
   2.187 -\hspace*{0pt}val monoidl{\char95}monoid = {\char35}monoidl{\char95}monoid :~'a monoid -> 'a monoidl;\\
   2.188 -\hspace*{0pt}\\
   2.189 -\hspace*{0pt}type 'a group = {\char123}monoid{\char95}group :~'a monoid,~inverse :~'a -> 'a{\char125};\\
   2.190 -\hspace*{0pt}val monoid{\char95}group = {\char35}monoid{\char95}group :~'a group -> 'a monoid;\\
   2.191 -\hspace*{0pt}val inverse = {\char35}inverse :~'a group -> 'a -> 'a;\\
   2.192 -\hspace*{0pt}\\
   2.193 -\hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\
   2.194 -\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\
   2.195 -\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\
   2.196 -\hspace*{0pt}\\
   2.197 -\hspace*{0pt}fun pow{\char95}int A{\char95}~k x =\\
   2.198 -\hspace*{0pt} ~(if IntInf.<= ((0 :~IntInf.int),~k)\\
   2.199 -\hspace*{0pt} ~~~then pow{\char95}nat (monoid{\char95}group A{\char95}) (nat k) x\\
   2.200 -\hspace*{0pt} ~~~else inverse A{\char95}~(pow{\char95}nat (monoid{\char95}group A{\char95}) (nat (IntInf.{\char126}~k)) x));\\
   2.201 -\hspace*{0pt}\\
   2.202 -\hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i,~j);\\
   2.203 -\hspace*{0pt}\\
   2.204 -\hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\
   2.205 -\hspace*{0pt}\\
   2.206 -\hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int);\\
   2.207 -\hspace*{0pt}\\
   2.208 -\hspace*{0pt}val monoidl{\char95}int =\\
   2.209 -\hspace*{0pt} ~{\char123}semigroup{\char95}monoidl = semigroup{\char95}int,~neutral = neutral{\char95}int{\char125}~:\\
   2.210 -\hspace*{0pt} ~IntInf.int monoidl;\\
   2.211 -\hspace*{0pt}\\
   2.212 -\hspace*{0pt}val monoid{\char95}int = {\char123}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:~IntInf.int monoid;\\
   2.213 -\hspace*{0pt}\\
   2.214 -\hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\
   2.215 -\hspace*{0pt}\\
   2.216 -\hspace*{0pt}val group{\char95}int = {\char123}monoid{\char95}group = monoid{\char95}int,~inverse = inverse{\char95}int{\char125}~:\\
   2.217 -\hspace*{0pt} ~IntInf.int group;\\
   2.218 -\hspace*{0pt}\\
   2.219 -\hspace*{0pt}val example :~IntInf.int =\\
   2.220 -\hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int);\\
   2.221 -\hspace*{0pt}\\
   2.222 -\hspace*{0pt}end;~(*struct Example*)%
   2.223 +\begin{typewriter}
   2.224 +    structure\ Example\ {\isacharcolon}\ sig\isanewline
   2.225 +\ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline
   2.226 +\ \ val\ nat{\isacharunderscore}aux\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ nat\isanewline
   2.227 +\ \ val\ nat\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ nat\isanewline
   2.228 +\ \ type\ {\isacharprime}a\ semigroup\isanewline
   2.229 +\ \ val\ mult\ {\isacharcolon}\ {\isacharprime}a\ semigroup\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
   2.230 +\ \ type\ {\isacharprime}a\ monoidl\isanewline
   2.231 +\ \ val\ semigroup{\isacharunderscore}monoidl\ {\isacharcolon}\ {\isacharprime}a\ monoidl\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ semigroup\isanewline
   2.232 +\ \ val\ neutral\ {\isacharcolon}\ {\isacharprime}a\ monoidl\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
   2.233 +\ \ type\ {\isacharprime}a\ monoid\isanewline
   2.234 +\ \ val\ monoidl{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ monoidl\isanewline
   2.235 +\ \ type\ {\isacharprime}a\ group\isanewline
   2.236 +\ \ val\ monoid{\isacharunderscore}group\ {\isacharcolon}\ {\isacharprime}a\ group\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ monoid\isanewline
   2.237 +\ \ val\ inverse\ {\isacharcolon}\ {\isacharprime}a\ group\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
   2.238 +\ \ val\ pow{\isacharunderscore}nat\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
   2.239 +\ \ val\ pow{\isacharunderscore}int\ {\isacharcolon}\ {\isacharprime}a\ group\ {\isacharminus}{\isachargreater}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
   2.240 +\ \ val\ mult{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ IntInf{\isachardot}int\isanewline
   2.241 +\ \ val\ semigroup{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ semigroup\isanewline
   2.242 +\ \ val\ neutral{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\isanewline
   2.243 +\ \ val\ monoidl{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ monoidl\isanewline
   2.244 +\ \ val\ monoid{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ monoid\isanewline
   2.245 +\ \ val\ inverse{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ IntInf{\isachardot}int\isanewline
   2.246 +\ \ val\ group{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ group\isanewline
   2.247 +\ \ val\ example\ {\isacharcolon}\ IntInf{\isachardot}int\isanewline
   2.248 +end\ {\isacharequal}\ struct\isanewline
   2.249 +\isanewline
   2.250 +datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat{\isacharsemicolon}\isanewline
   2.251 +\isanewline
   2.252 +fun\ nat{\isacharunderscore}aux\ i\ n\ {\isacharequal}\isanewline
   2.253 +\ \ {\isacharparenleft}if\ IntInf{\isachardot}{\isacharless}{\isacharequal}\ {\isacharparenleft}i{\isacharcomma}\ {\isacharparenleft}{\isadigit{0}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}{\isacharparenright}\ then\ n\isanewline
   2.254 +\ \ \ \ 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
   2.255 +\isanewline
   2.256 +fun\ nat\ i\ {\isacharequal}\ nat{\isacharunderscore}aux\ i\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline
   2.257 +\isanewline
   2.258 +type\ {\isacharprime}a\ semigroup\ {\isacharequal}\ {\isacharbraceleft}mult\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharbraceright}{\isacharsemicolon}\isanewline
   2.259 +val\ mult\ {\isacharequal}\ {\isacharhash}mult\ {\isacharcolon}\ {\isacharprime}a\ semigroup\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharsemicolon}\isanewline
   2.260 +\isanewline
   2.261 +type\ {\isacharprime}a\ monoidl\ {\isacharequal}\ {\isacharbraceleft}semigroup{\isacharunderscore}monoidl\ {\isacharcolon}\ {\isacharprime}a\ semigroup{\isacharcomma}\ neutral\ {\isacharcolon}\ {\isacharprime}a{\isacharbraceright}{\isacharsemicolon}\isanewline
   2.262 +val\ semigroup{\isacharunderscore}monoidl\ {\isacharequal}\ {\isacharhash}semigroup{\isacharunderscore}monoidl\ {\isacharcolon}\ {\isacharprime}a\ monoidl\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ semigroup{\isacharsemicolon}\isanewline
   2.263 +val\ neutral\ {\isacharequal}\ {\isacharhash}neutral\ {\isacharcolon}\ {\isacharprime}a\ monoidl\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharsemicolon}\isanewline
   2.264 +\isanewline
   2.265 +type\ {\isacharprime}a\ monoid\ {\isacharequal}\ {\isacharbraceleft}monoidl{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ monoidl{\isacharbraceright}{\isacharsemicolon}\isanewline
   2.266 +val\ monoidl{\isacharunderscore}monoid\ {\isacharequal}\ {\isacharhash}monoidl{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ monoidl{\isacharsemicolon}\isanewline
   2.267 +\isanewline
   2.268 +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
   2.269 +val\ monoid{\isacharunderscore}group\ {\isacharequal}\ {\isacharhash}monoid{\isacharunderscore}group\ {\isacharcolon}\ {\isacharprime}a\ group\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ monoid{\isacharsemicolon}\isanewline
   2.270 +val\ inverse\ {\isacharequal}\ {\isacharhash}inverse\ {\isacharcolon}\ {\isacharprime}a\ group\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharsemicolon}\isanewline
   2.271 +\isanewline
   2.272 +fun\ pow{\isacharunderscore}nat\ A{\isacharunderscore}\ Zero{\isacharunderscore}nat\ x\ {\isacharequal}\ neutral\ {\isacharparenleft}monoidl{\isacharunderscore}monoid\ A{\isacharunderscore}{\isacharparenright}\isanewline
   2.273 +\ \ {\isacharbar}\ pow{\isacharunderscore}nat\ A{\isacharunderscore}\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\isanewline
   2.274 +\ \ \ \ 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
   2.275 +\isanewline
   2.276 +fun\ pow{\isacharunderscore}int\ A{\isacharunderscore}\ k\ x\ {\isacharequal}\isanewline
   2.277 +\ \ {\isacharparenleft}if\ IntInf{\isachardot}{\isacharless}{\isacharequal}\ {\isacharparenleft}{\isacharparenleft}{\isadigit{0}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}{\isacharcomma}\ k{\isacharparenright}\isanewline
   2.278 +\ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}monoid{\isacharunderscore}group\ A{\isacharunderscore}{\isacharparenright}\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
   2.279 +\ \ \ \ 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
   2.280 +\isanewline
   2.281 +fun\ mult{\isacharunderscore}int\ i\ j\ {\isacharequal}\ IntInf{\isachardot}{\isacharplus}\ {\isacharparenleft}i{\isacharcomma}\ j{\isacharparenright}{\isacharsemicolon}\isanewline
   2.282 +\isanewline
   2.283 +val\ semigroup{\isacharunderscore}int\ {\isacharequal}\ {\isacharbraceleft}mult\ {\isacharequal}\ mult{\isacharunderscore}int{\isacharbraceright}\ {\isacharcolon}\ IntInf{\isachardot}int\ semigroup{\isacharsemicolon}\isanewline
   2.284 +\isanewline
   2.285 +val\ neutral{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}{\isacharsemicolon}\isanewline
   2.286 +\isanewline
   2.287 +val\ monoidl{\isacharunderscore}int\ {\isacharequal}\isanewline
   2.288 +\ \ {\isacharbraceleft}semigroup{\isacharunderscore}monoidl\ {\isacharequal}\ semigroup{\isacharunderscore}int{\isacharcomma}\ neutral\ {\isacharequal}\ neutral{\isacharunderscore}int{\isacharbraceright}\ {\isacharcolon}\isanewline
   2.289 +\ \ IntInf{\isachardot}int\ monoidl{\isacharsemicolon}\isanewline
   2.290 +\isanewline
   2.291 +val\ monoid{\isacharunderscore}int\ {\isacharequal}\ {\isacharbraceleft}monoidl{\isacharunderscore}monoid\ {\isacharequal}\ monoidl{\isacharunderscore}int{\isacharbraceright}\ {\isacharcolon}\ IntInf{\isachardot}int\ monoid{\isacharsemicolon}\isanewline
   2.292 +\isanewline
   2.293 +fun\ inverse{\isacharunderscore}int\ i\ {\isacharequal}\ IntInf{\isachardot}{\isachartilde}\ i{\isacharsemicolon}\isanewline
   2.294 +\isanewline
   2.295 +val\ group{\isacharunderscore}int\ {\isacharequal}\ {\isacharbraceleft}monoid{\isacharunderscore}group\ {\isacharequal}\ monoid{\isacharunderscore}int{\isacharcomma}\ inverse\ {\isacharequal}\ inverse{\isacharunderscore}int{\isacharbraceright}\ {\isacharcolon}\isanewline
   2.296 +\ \ IntInf{\isachardot}int\ group{\isacharsemicolon}\isanewline
   2.297 +\isanewline
   2.298 +val\ example\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharequal}\isanewline
   2.299 +\ \ 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
   2.300 +\isanewline
   2.301 +end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline
   2.302 +
   2.303 +  \end{typewriter}%
   2.304  \end{isamarkuptext}%
   2.305  \isamarkuptrue%
   2.306  %
   2.307 @@ -1331,76 +1333,77 @@
   2.308  \isatagquote
   2.309  %
   2.310  \begin{isamarkuptext}%
   2.311 -\isatypewriter%
   2.312 -\noindent%
   2.313 -\hspace*{0pt}object Example {\char123}\\
   2.314 -\hspace*{0pt}\\
   2.315 -\hspace*{0pt}abstract sealed class nat\\
   2.316 -\hspace*{0pt}final case object Zero{\char95}nat extends nat\\
   2.317 -\hspace*{0pt}final case class Suc(a:~nat) extends nat\\
   2.318 -\hspace*{0pt}\\
   2.319 -\hspace*{0pt}def nat{\char95}aux(i:~BigInt,~n:~nat):~nat =\\
   2.320 -\hspace*{0pt} ~(if (i <= BigInt(0)) n else nat{\char95}aux(i - BigInt(1),~Suc(n)))\\
   2.321 -\hspace*{0pt}\\
   2.322 -\hspace*{0pt}def nat(i:~BigInt):~nat = nat{\char95}aux(i,~Zero{\char95}nat)\\
   2.323 -\hspace*{0pt}\\
   2.324 -\hspace*{0pt}trait semigroup[A] {\char123}\\
   2.325 -\hspace*{0pt} ~val `Example.mult`:~(A,~A) => A\\
   2.326 -\hspace*{0pt}{\char125}\\
   2.327 -\hspace*{0pt}def mult[A](a:~A,~b:~A)(implicit A:~semigroup[A]):~A =\\
   2.328 -\hspace*{0pt} ~A.`Example.mult`(a,~b)\\
   2.329 -\hspace*{0pt}\\
   2.330 -\hspace*{0pt}trait monoidl[A] extends semigroup[A] {\char123}\\
   2.331 -\hspace*{0pt} ~val `Example.neutral`:~A\\
   2.332 -\hspace*{0pt}{\char125}\\
   2.333 -\hspace*{0pt}def neutral[A](implicit A:~monoidl[A]):~A = A.`Example.neutral`\\
   2.334 -\hspace*{0pt}\\
   2.335 -\hspace*{0pt}trait monoid[A] extends monoidl[A] {\char123}\\
   2.336 -\hspace*{0pt}{\char125}\\
   2.337 -\hspace*{0pt}\\
   2.338 -\hspace*{0pt}trait group[A] extends monoid[A] {\char123}\\
   2.339 -\hspace*{0pt} ~val `Example.inverse`:~A => A\\
   2.340 -\hspace*{0pt}{\char125}\\
   2.341 -\hspace*{0pt}def inverse[A](a:~A)(implicit A:~group[A]):~A = A.`Example.inverse`(a)\\
   2.342 -\hspace*{0pt}\\
   2.343 -\hspace*{0pt}def pow{\char95}nat[A:~monoid](xa0:~nat,~x:~A):~A = (xa0,~x) match {\char123}\\
   2.344 -\hspace*{0pt} ~case (Zero{\char95}nat,~x) => neutral[A]\\
   2.345 -\hspace*{0pt} ~case (Suc(n),~x) => mult[A](x,~pow{\char95}nat[A](n,~x))\\
   2.346 -\hspace*{0pt}{\char125}\\
   2.347 -\hspace*{0pt}\\
   2.348 -\hspace*{0pt}def pow{\char95}int[A:~group](k:~BigInt,~x:~A):~A =\\
   2.349 -\hspace*{0pt} ~(if (BigInt(0) <= k) pow{\char95}nat[A](nat(k),~x)\\
   2.350 -\hspace*{0pt} ~~~else inverse[A](pow{\char95}nat[A](nat((- k)),~x)))\\
   2.351 -\hspace*{0pt}\\
   2.352 -\hspace*{0pt}def mult{\char95}int(i:~BigInt,~j:~BigInt):~BigInt = i + j\\
   2.353 -\hspace*{0pt}\\
   2.354 -\hspace*{0pt}implicit def semigroup{\char95}int:~semigroup[BigInt] = new semigroup[BigInt] {\char123}\\
   2.355 -\hspace*{0pt} ~val `Example.mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\
   2.356 -\hspace*{0pt}{\char125}\\
   2.357 -\hspace*{0pt}\\
   2.358 -\hspace*{0pt}def neutral{\char95}int:~BigInt = BigInt(0)\\
   2.359 -\hspace*{0pt}\\
   2.360 -\hspace*{0pt}implicit def monoidl{\char95}int:~monoidl[BigInt] = new monoidl[BigInt] {\char123}\\
   2.361 -\hspace*{0pt} ~val `Example.neutral` = neutral{\char95}int\\
   2.362 -\hspace*{0pt} ~val `Example.mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\
   2.363 -\hspace*{0pt}{\char125}\\
   2.364 -\hspace*{0pt}\\
   2.365 -\hspace*{0pt}implicit def monoid{\char95}int:~monoid[BigInt] = new monoid[BigInt] {\char123}\\
   2.366 -\hspace*{0pt} ~val `Example.neutral` = neutral{\char95}int\\
   2.367 -\hspace*{0pt} ~val `Example.mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\
   2.368 -\hspace*{0pt}{\char125}\\
   2.369 -\hspace*{0pt}\\
   2.370 -\hspace*{0pt}def inverse{\char95}int(i:~BigInt):~BigInt = (- i)\\
   2.371 -\hspace*{0pt}\\
   2.372 -\hspace*{0pt}implicit def group{\char95}int:~group[BigInt] = new group[BigInt] {\char123}\\
   2.373 -\hspace*{0pt} ~val `Example.inverse` = (a:~BigInt) => inverse{\char95}int(a)\\
   2.374 -\hspace*{0pt} ~val `Example.neutral` = neutral{\char95}int\\
   2.375 -\hspace*{0pt} ~val `Example.mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\
   2.376 -\hspace*{0pt}{\char125}\\
   2.377 -\hspace*{0pt}\\
   2.378 -\hspace*{0pt}def example:~BigInt = pow{\char95}int[BigInt](BigInt(10),~BigInt(- 2))\\
   2.379 -\hspace*{0pt}\\
   2.380 -\hspace*{0pt}{\char125}~/* object Example */%
   2.381 +\begin{typewriter}
   2.382 +    object\ Example\ {\isacharbraceleft}\isanewline
   2.383 +\isanewline
   2.384 +abstract\ sealed\ class\ nat\isanewline
   2.385 +final\ case\ object\ Zero{\isacharunderscore}nat\ extends\ nat\isanewline
   2.386 +final\ case\ class\ Suc{\isacharparenleft}a{\isacharcolon}\ nat{\isacharparenright}\ extends\ nat\isanewline
   2.387 +\isanewline
   2.388 +def\ nat{\isacharunderscore}aux{\isacharparenleft}i{\isacharcolon}\ BigInt{\isacharcomma}\ n{\isacharcolon}\ nat{\isacharparenright}{\isacharcolon}\ nat\ {\isacharequal}\isanewline
   2.389 +\ \ {\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
   2.390 +\isanewline
   2.391 +def\ nat{\isacharparenleft}i{\isacharcolon}\ BigInt{\isacharparenright}{\isacharcolon}\ nat\ {\isacharequal}\ nat{\isacharunderscore}aux{\isacharparenleft}i{\isacharcomma}\ Zero{\isacharunderscore}nat{\isacharparenright}\isanewline
   2.392 +\isanewline
   2.393 +trait\ semigroup{\isacharbrackleft}A{\isacharbrackright}\ {\isacharbraceleft}\isanewline
   2.394 +\ \ val\ {\isacharbackquote}Example{\isachardot}mult{\isacharbackquote}{\isacharcolon}\ {\isacharparenleft}A{\isacharcomma}\ A{\isacharparenright}\ {\isacharequal}{\isachargreater}\ A\isanewline
   2.395 +{\isacharbraceright}\isanewline
   2.396 +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
   2.397 +\ \ A{\isachardot}{\isacharbackquote}Example{\isachardot}mult{\isacharbackquote}{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\isanewline
   2.398 +\isanewline
   2.399 +trait\ monoidl{\isacharbrackleft}A{\isacharbrackright}\ extends\ semigroup{\isacharbrackleft}A{\isacharbrackright}\ {\isacharbraceleft}\isanewline
   2.400 +\ \ val\ {\isacharbackquote}Example{\isachardot}neutral{\isacharbackquote}{\isacharcolon}\ A\isanewline
   2.401 +{\isacharbraceright}\isanewline
   2.402 +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
   2.403 +\isanewline
   2.404 +trait\ monoid{\isacharbrackleft}A{\isacharbrackright}\ extends\ monoidl{\isacharbrackleft}A{\isacharbrackright}\ {\isacharbraceleft}\isanewline
   2.405 +{\isacharbraceright}\isanewline
   2.406 +\isanewline
   2.407 +trait\ group{\isacharbrackleft}A{\isacharbrackright}\ extends\ monoid{\isacharbrackleft}A{\isacharbrackright}\ {\isacharbraceleft}\isanewline
   2.408 +\ \ val\ {\isacharbackquote}Example{\isachardot}inverse{\isacharbackquote}{\isacharcolon}\ A\ {\isacharequal}{\isachargreater}\ A\isanewline
   2.409 +{\isacharbraceright}\isanewline
   2.410 +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
   2.411 +\isanewline
   2.412 +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
   2.413 +\ \ case\ {\isacharparenleft}Zero{\isacharunderscore}nat{\isacharcomma}\ x{\isacharparenright}\ {\isacharequal}{\isachargreater}\ neutral{\isacharbrackleft}A{\isacharbrackright}\isanewline
   2.414 +\ \ 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
   2.415 +{\isacharbraceright}\isanewline
   2.416 +\isanewline
   2.417 +def\ pow{\isacharunderscore}int{\isacharbrackleft}A{\isacharcolon}\ group{\isacharbrackright}{\isacharparenleft}k{\isacharcolon}\ BigInt{\isacharcomma}\ x{\isacharcolon}\ A{\isacharparenright}{\isacharcolon}\ A\ {\isacharequal}\isanewline
   2.418 +\ \ {\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
   2.419 +\ \ \ \ 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
   2.420 +\isanewline
   2.421 +def\ mult{\isacharunderscore}int{\isacharparenleft}i{\isacharcolon}\ BigInt{\isacharcomma}\ j{\isacharcolon}\ BigInt{\isacharparenright}{\isacharcolon}\ BigInt\ {\isacharequal}\ i\ {\isacharplus}\ j\isanewline
   2.422 +\isanewline
   2.423 +implicit\ def\ semigroup{\isacharunderscore}int{\isacharcolon}\ semigroup{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharequal}\ new\ semigroup{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharbraceleft}\isanewline
   2.424 +\ \ 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
   2.425 +{\isacharbraceright}\isanewline
   2.426 +\isanewline
   2.427 +def\ neutral{\isacharunderscore}int{\isacharcolon}\ BigInt\ {\isacharequal}\ BigInt{\isacharparenleft}{\isadigit{0}}{\isacharparenright}\isanewline
   2.428 +\isanewline
   2.429 +implicit\ def\ monoidl{\isacharunderscore}int{\isacharcolon}\ monoidl{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharequal}\ new\ monoidl{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharbraceleft}\isanewline
   2.430 +\ \ val\ {\isacharbackquote}Example{\isachardot}neutral{\isacharbackquote}\ {\isacharequal}\ neutral{\isacharunderscore}int\isanewline
   2.431 +\ \ 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
   2.432 +{\isacharbraceright}\isanewline
   2.433 +\isanewline
   2.434 +implicit\ def\ monoid{\isacharunderscore}int{\isacharcolon}\ monoid{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharequal}\ new\ monoid{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharbraceleft}\isanewline
   2.435 +\ \ val\ {\isacharbackquote}Example{\isachardot}neutral{\isacharbackquote}\ {\isacharequal}\ neutral{\isacharunderscore}int\isanewline
   2.436 +\ \ 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
   2.437 +{\isacharbraceright}\isanewline
   2.438 +\isanewline
   2.439 +def\ inverse{\isacharunderscore}int{\isacharparenleft}i{\isacharcolon}\ BigInt{\isacharparenright}{\isacharcolon}\ BigInt\ {\isacharequal}\ {\isacharparenleft}{\isacharminus}\ i{\isacharparenright}\isanewline
   2.440 +\isanewline
   2.441 +implicit\ def\ group{\isacharunderscore}int{\isacharcolon}\ group{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharequal}\ new\ group{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharbraceleft}\isanewline
   2.442 +\ \ val\ {\isacharbackquote}Example{\isachardot}inverse{\isacharbackquote}\ {\isacharequal}\ {\isacharparenleft}a{\isacharcolon}\ BigInt{\isacharparenright}\ {\isacharequal}{\isachargreater}\ inverse{\isacharunderscore}int{\isacharparenleft}a{\isacharparenright}\isanewline
   2.443 +\ \ val\ {\isacharbackquote}Example{\isachardot}neutral{\isacharbackquote}\ {\isacharequal}\ neutral{\isacharunderscore}int\isanewline
   2.444 +\ \ 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
   2.445 +{\isacharbraceright}\isanewline
   2.446 +\isanewline
   2.447 +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
   2.448 +\isanewline
   2.449 +{\isacharbraceright}\ {\isacharslash}{\isacharasterisk}\ object\ Example\ {\isacharasterisk}{\isacharslash}\isanewline
   2.450 +
   2.451 +  \end{typewriter}%
   2.452  \end{isamarkuptext}%
   2.453  \isamarkuptrue%
   2.454  %
     3.1 --- a/doc-src/Classes/style.sty	Thu Sep 23 13:28:53 2010 +0200
     3.2 +++ b/doc-src/Classes/style.sty	Thu Sep 23 15:46:17 2010 +0200
     3.3 @@ -26,6 +26,12 @@
     3.4  \renewcommand{\endisatagquote}{\end{quote}}
     3.5  \newcommand{\quotebreak}{\\[1.2ex]}
     3.6  
     3.7 +%% typewriter text
     3.8 +\newenvironment{typewriter}{\renewcommand{\isadigit}[1]{{##1}}%
     3.9 +\def\isacharunderscore{\_}%
    3.10 +\parindent0pt\fontsize{9pt}{0pt}%
    3.11 +\tt\setlength{\baselineskip}{8pt}\renewcommand{\baselinestretch}{1}}{}
    3.12 +
    3.13  %% presentation
    3.14  \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
    3.15  
     4.1 --- a/doc-src/Codegen/Thy/Adaptation.thy	Thu Sep 23 13:28:53 2010 +0200
     4.2 +++ b/doc-src/Codegen/Thy/Adaptation.thy	Thu Sep 23 15:46:17 2010 +0200
     4.3 @@ -175,7 +175,11 @@
     4.4  code_const %invisible True and False and "op \<and>" and Not
     4.5    (SML and and and)
     4.6  (*>*)
     4.7 -text %quote {*@{code_stmts in_interval (SML)}*}
     4.8 +text %quote {*
     4.9 +  \begin{typewriter}
    4.10 +    @{code_stmts in_interval (SML)}
    4.11 +  \end{typewriter}
    4.12 +*}
    4.13  
    4.14  text {*
    4.15    \noindent Though this is correct code, it is a little bit
    4.16 @@ -204,7 +208,11 @@
    4.17    placeholder for the type constructor's (the constant's) arguments.
    4.18  *}
    4.19  
    4.20 -text %quote {*@{code_stmts in_interval (SML)}*}
    4.21 +text %quote {*
    4.22 +  \begin{typewriter}
    4.23 +    @{code_stmts in_interval (SML)}
    4.24 +  \end{typewriter}
    4.25 +*}
    4.26  
    4.27  text {*
    4.28    \noindent This still is not perfect: the parentheses around the
    4.29 @@ -217,7 +225,11 @@
    4.30  code_const %quotett "op \<and>"
    4.31    (SML infixl 1 "andalso")
    4.32  
    4.33 -text %quote {*@{code_stmts in_interval (SML)}*}
    4.34 +text %quote {*
    4.35 +  \begin{typewriter}
    4.36 +    @{code_stmts in_interval (SML)}
    4.37 +  \end{typewriter}
    4.38 +*}
    4.39  
    4.40  text {*
    4.41    \noindent The attentive reader may ask how we assert that no
     5.1 --- a/doc-src/Codegen/Thy/Foundations.thy	Thu Sep 23 13:28:53 2010 +0200
     5.2 +++ b/doc-src/Codegen/Thy/Foundations.thy	Thu Sep 23 15:46:17 2010 +0200
     5.3 @@ -161,7 +161,11 @@
     5.4    is determined syntactically.  The resulting code:
     5.5  *}
     5.6  
     5.7 -text %quote {*@{code_stmts dequeue (consts) dequeue (Haskell)}*}
     5.8 +text %quote {*
     5.9 +  \begin{typewriter}
    5.10 +    @{code_stmts dequeue (consts) dequeue (Haskell)}
    5.11 +  \end{typewriter}
    5.12 +*}
    5.13  
    5.14  text {*
    5.15    \noindent You may note that the equality test @{term "xs = []"} has
    5.16 @@ -215,7 +219,11 @@
    5.17    equality check, as can be seen in the corresponding @{text SML} code:
    5.18  *}
    5.19  
    5.20 -text %quote {*@{code_stmts collect_duplicates (SML)}*}
    5.21 +text %quote {*
    5.22 +  \begin{typewriter}
    5.23 +    @{code_stmts collect_duplicates (SML)}
    5.24 +  \end{typewriter}
    5.25 +*}
    5.26  
    5.27  text {*
    5.28    \noindent Obviously, polymorphic equality is implemented the Haskell
    5.29 @@ -251,7 +259,11 @@
    5.30    for the pattern @{term "AQueue [] []"}:
    5.31  *}
    5.32  
    5.33 -text %quote {*@{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}*}
    5.34 +text %quote {*
    5.35 +  \begin{typewriter}
    5.36 +    @{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}
    5.37 +  \end{typewriter}
    5.38 +*}
    5.39  
    5.40  text {*
    5.41    \noindent In some cases it is desirable to have this
    5.42 @@ -290,7 +302,11 @@
    5.43    exception at the appropriate position:
    5.44  *}
    5.45  
    5.46 -text %quote {*@{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}*}
    5.47 +text %quote {*
    5.48 +  \begin{typewriter}
    5.49 +    @{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}
    5.50 +  \end{typewriter}
    5.51 +*}
    5.52  
    5.53  text {*
    5.54    \noindent This feature however is rarely needed in practice.  Note
     6.1 --- a/doc-src/Codegen/Thy/Further.thy	Thu Sep 23 13:28:53 2010 +0200
     6.2 +++ b/doc-src/Codegen/Thy/Further.thy	Thu Sep 23 15:46:17 2010 +0200
     6.3 @@ -112,7 +112,11 @@
     6.4    After this setup procedure, code generation can continue as usual:
     6.5  *}
     6.6  
     6.7 -text %quote {*@{code_stmts funpows (consts) Nat.funpow funpows (Haskell)}*}
     6.8 +text %quote {*
     6.9 +  \begin{typewriter}
    6.10 +    @{code_stmts funpows (consts) Nat.funpow funpows (Haskell)}
    6.11 +  \end{typewriter}
    6.12 +*}
    6.13  
    6.14  
    6.15  subsection {* Imperative data structures *}
     7.1 --- a/doc-src/Codegen/Thy/Introduction.thy	Thu Sep 23 13:28:53 2010 +0200
     7.2 +++ b/doc-src/Codegen/Thy/Introduction.thy	Thu Sep 23 15:46:17 2010 +0200
     7.3 @@ -70,7 +70,11 @@
     7.4  
     7.5  text {* \noindent resulting in the following code: *}
     7.6  
     7.7 -text %quote {*@{code_stmts empty enqueue dequeue (SML)}*}
     7.8 +text %quote {*
     7.9 +  \begin{typewriter}
    7.10 +    @{code_stmts empty enqueue dequeue (SML)}
    7.11 +  \end{typewriter}
    7.12 +*}
    7.13  
    7.14  text {*
    7.15    \noindent The @{command_def export_code} command takes a
    7.16 @@ -91,7 +95,11 @@
    7.17    \noindent This is the corresponding code:
    7.18  *}
    7.19  
    7.20 -text %quote {*@{code_stmts empty enqueue dequeue (Haskell)}*}
    7.21 +text %quote {*
    7.22 +  \begin{typewriter}
    7.23 +    @{code_stmts empty enqueue dequeue (Haskell)}
    7.24 +  \end{typewriter}
    7.25 +*}
    7.26  
    7.27  text {*
    7.28    \noindent For more details about @{command export_code} see
    7.29 @@ -164,7 +172,11 @@
    7.30    native classes:
    7.31  *}
    7.32  
    7.33 -text %quote {*@{code_stmts bexp (Haskell)}*}
    7.34 +text %quote {*
    7.35 +  \begin{typewriter}
    7.36 +    @{code_stmts bexp (Haskell)}
    7.37 +  \end{typewriter}
    7.38 +*}
    7.39  
    7.40  text {*
    7.41    \noindent This is a convenient place to show how explicit dictionary
    7.42 @@ -172,7 +184,11 @@
    7.43    @{text SML}:
    7.44  *}
    7.45  
    7.46 -text %quote {*@{code_stmts bexp (SML)}*}
    7.47 +text %quote {*
    7.48 +  \begin{typewriter}
    7.49 +    @{code_stmts bexp (SML)}
    7.50 +  \end{typewriter}
    7.51 +*}
    7.52  
    7.53  text {*
    7.54    \noindent Note the parameters with trailing underscore (@{verbatim
     8.1 --- a/doc-src/Codegen/Thy/Refinement.thy	Thu Sep 23 13:28:53 2010 +0200
     8.2 +++ b/doc-src/Codegen/Thy/Refinement.thy	Thu Sep 23 15:46:17 2010 +0200
     8.3 @@ -31,7 +31,11 @@
     8.4    to two recursive calls:
     8.5  *}
     8.6  
     8.7 -text %quote {*@{code_stmts fib (consts) fib (Haskell)}*}
     8.8 +text %quote {*
     8.9 +  \begin{typewriter}
    8.10 +    @{code_stmts fib (consts) fib (Haskell)}
    8.11 +  \end{typewriter}
    8.12 +*}
    8.13  
    8.14  text {*
    8.15    \noindent A more efficient implementation would use dynamic
    8.16 @@ -67,7 +71,11 @@
    8.17    \noindent The resulting code shows only linear growth of runtime:
    8.18  *}
    8.19  
    8.20 -text %quote {*@{code_stmts fib (consts) fib fib_step (Haskell)}*}
    8.21 +text %quote {*
    8.22 +  \begin{typewriter}
    8.23 +    @{code_stmts fib (consts) fib fib_step (Haskell)}
    8.24 +  \end{typewriter}
    8.25 +*}
    8.26  
    8.27  
    8.28  subsection {* Datatype refinement *}
    8.29 @@ -153,7 +161,11 @@
    8.30    \noindent The resulting code looks as expected:
    8.31  *}
    8.32  
    8.33 -text %quote {*@{code_stmts empty enqueue dequeue (SML)}*}
    8.34 +text %quote {*
    8.35 +  \begin{typewriter}
    8.36 +    @{code_stmts empty enqueue dequeue (SML)}
    8.37 +  \end{typewriter}
    8.38 +*}
    8.39  
    8.40  text {*
    8.41    The same techniques can also be applied to types which are not
    8.42 @@ -248,7 +260,9 @@
    8.43  *}
    8.44  
    8.45  text %quote {*
    8.46 -  @{code_stmts Dlist.empty Dlist.insert Dlist.remove list_of_dlist (Haskell)}
    8.47 +  \begin{typewriter}
    8.48 +    @{code_stmts Dlist.empty Dlist.insert Dlist.remove list_of_dlist (Haskell)}
    8.49 +  \end{typewriter}
    8.50  *} (*(types) dlist (consts) dempty dinsert dremove list_of List.member insert remove *)
    8.51  
    8.52  text {*
     9.1 --- a/doc-src/Codegen/Thy/document/Adaptation.tex	Thu Sep 23 13:28:53 2010 +0200
     9.2 +++ b/doc-src/Codegen/Thy/document/Adaptation.tex	Thu Sep 23 15:46:17 2010 +0200
     9.3 @@ -235,34 +235,35 @@
     9.4  \isatagquote
     9.5  %
     9.6  \begin{isamarkuptext}%
     9.7 -\isatypewriter%
     9.8 -\noindent%
     9.9 -\hspace*{0pt}structure Example :~sig\\
    9.10 -\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
    9.11 -\hspace*{0pt} ~datatype boola = True | False\\
    9.12 -\hspace*{0pt} ~val conj :~boola -> boola -> boola\\
    9.13 -\hspace*{0pt} ~val less{\char95}nat :~nat -> nat -> boola\\
    9.14 -\hspace*{0pt} ~val less{\char95}eq{\char95}nat :~nat -> nat -> boola\\
    9.15 -\hspace*{0pt} ~val in{\char95}interval :~nat * nat -> nat -> boola\\
    9.16 -\hspace*{0pt}end = struct\\
    9.17 -\hspace*{0pt}\\
    9.18 -\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
    9.19 -\hspace*{0pt}\\
    9.20 -\hspace*{0pt}datatype boola = True | False;\\
    9.21 -\hspace*{0pt}\\
    9.22 -\hspace*{0pt}fun conj p True = p\\
    9.23 -\hspace*{0pt} ~| conj p False = False\\
    9.24 -\hspace*{0pt} ~| conj True p = p\\
    9.25 -\hspace*{0pt} ~| conj False p = False;\\
    9.26 -\hspace*{0pt}\\
    9.27 -\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
    9.28 -\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = False\\
    9.29 -\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
    9.30 -\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = True;\\
    9.31 -\hspace*{0pt}\\
    9.32 -\hspace*{0pt}fun in{\char95}interval (k,~l) n = conj (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\
    9.33 -\hspace*{0pt}\\
    9.34 -\hspace*{0pt}end;~(*struct Example*)%
    9.35 +\begin{typewriter}
    9.36 +    structure\ Example\ {\isacharcolon}\ sig\isanewline
    9.37 +\ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline
    9.38 +\ \ datatype\ boola\ {\isacharequal}\ True\ {\isacharbar}\ False\isanewline
    9.39 +\ \ val\ conj\ {\isacharcolon}\ boola\ {\isacharminus}{\isachargreater}\ boola\ {\isacharminus}{\isachargreater}\ boola\isanewline
    9.40 +\ \ val\ less{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ boola\isanewline
    9.41 +\ \ val\ less{\isacharunderscore}eq{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ boola\isanewline
    9.42 +\ \ val\ in{\isacharunderscore}interval\ {\isacharcolon}\ nat\ {\isacharasterisk}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ boola\isanewline
    9.43 +end\ {\isacharequal}\ struct\isanewline
    9.44 +\isanewline
    9.45 +datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat{\isacharsemicolon}\isanewline
    9.46 +\isanewline
    9.47 +datatype\ boola\ {\isacharequal}\ True\ {\isacharbar}\ False{\isacharsemicolon}\isanewline
    9.48 +\isanewline
    9.49 +fun\ conj\ p\ True\ {\isacharequal}\ p\isanewline
    9.50 +\ \ {\isacharbar}\ conj\ p\ False\ {\isacharequal}\ False\isanewline
    9.51 +\ \ {\isacharbar}\ conj\ True\ p\ {\isacharequal}\ p\isanewline
    9.52 +\ \ {\isacharbar}\ conj\ False\ p\ {\isacharequal}\ False{\isacharsemicolon}\isanewline
    9.53 +\isanewline
    9.54 +fun\ less{\isacharunderscore}nat\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ less{\isacharunderscore}eq{\isacharunderscore}nat\ m\ n\isanewline
    9.55 +\ \ {\isacharbar}\ less{\isacharunderscore}nat\ n\ Zero{\isacharunderscore}nat\ {\isacharequal}\ False\isanewline
    9.56 +and\ less{\isacharunderscore}eq{\isacharunderscore}nat\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n\ {\isacharequal}\ less{\isacharunderscore}nat\ m\ n\isanewline
    9.57 +\ \ {\isacharbar}\ less{\isacharunderscore}eq{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ n\ {\isacharequal}\ True{\isacharsemicolon}\isanewline
    9.58 +\isanewline
    9.59 +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
    9.60 +\isanewline
    9.61 +end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline
    9.62 +
    9.63 +  \end{typewriter}%
    9.64  \end{isamarkuptext}%
    9.65  \isamarkuptrue%
    9.66  %
    9.67 @@ -320,25 +321,26 @@
    9.68  \isatagquote
    9.69  %
    9.70  \begin{isamarkuptext}%
    9.71 -\isatypewriter%
    9.72 -\noindent%
    9.73 -\hspace*{0pt}structure Example :~sig\\
    9.74 -\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
    9.75 -\hspace*{0pt} ~val less{\char95}nat :~nat -> nat -> bool\\
    9.76 -\hspace*{0pt} ~val less{\char95}eq{\char95}nat :~nat -> nat -> bool\\
    9.77 -\hspace*{0pt} ~val in{\char95}interval :~nat * nat -> nat -> bool\\
    9.78 -\hspace*{0pt}end = struct\\
    9.79 -\hspace*{0pt}\\
    9.80 -\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
    9.81 -\hspace*{0pt}\\
    9.82 -\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
    9.83 -\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
    9.84 -\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
    9.85 -\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
    9.86 -\hspace*{0pt}\\
    9.87 -\hspace*{0pt}fun in{\char95}interval (k,~l) n = (less{\char95}eq{\char95}nat k n) andalso (less{\char95}eq{\char95}nat n l);\\
    9.88 -\hspace*{0pt}\\
    9.89 -\hspace*{0pt}end;~(*struct Example*)%
    9.90 +\begin{typewriter}
    9.91 +    structure\ Example\ {\isacharcolon}\ sig\isanewline
    9.92 +\ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline
    9.93 +\ \ val\ less{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline
    9.94 +\ \ val\ less{\isacharunderscore}eq{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline
    9.95 +\ \ val\ in{\isacharunderscore}interval\ {\isacharcolon}\ nat\ {\isacharasterisk}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline
    9.96 +end\ {\isacharequal}\ struct\isanewline
    9.97 +\isanewline
    9.98 +datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat{\isacharsemicolon}\isanewline
    9.99 +\isanewline
   9.100 +fun\ less{\isacharunderscore}nat\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ less{\isacharunderscore}eq{\isacharunderscore}nat\ m\ n\isanewline
   9.101 +\ \ {\isacharbar}\ less{\isacharunderscore}nat\ n\ Zero{\isacharunderscore}nat\ {\isacharequal}\ false\isanewline
   9.102 +and\ less{\isacharunderscore}eq{\isacharunderscore}nat\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n\ {\isacharequal}\ less{\isacharunderscore}nat\ m\ n\isanewline
   9.103 +\ \ {\isacharbar}\ less{\isacharunderscore}eq{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ n\ {\isacharequal}\ true{\isacharsemicolon}\isanewline
   9.104 +\isanewline
   9.105 +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
   9.106 +\isanewline
   9.107 +end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline
   9.108 +
   9.109 +  \end{typewriter}%
   9.110  \end{isamarkuptext}%
   9.111  \isamarkuptrue%
   9.112  %
   9.113 @@ -380,25 +382,26 @@
   9.114  \isatagquote
   9.115  %
   9.116  \begin{isamarkuptext}%
   9.117 -\isatypewriter%
   9.118 -\noindent%
   9.119 -\hspace*{0pt}structure Example :~sig\\
   9.120 -\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
   9.121 -\hspace*{0pt} ~val less{\char95}nat :~nat -> nat -> bool\\
   9.122 -\hspace*{0pt} ~val less{\char95}eq{\char95}nat :~nat -> nat -> bool\\
   9.123 -\hspace*{0pt} ~val in{\char95}interval :~nat * nat -> nat -> bool\\
   9.124 -\hspace*{0pt}end = struct\\
   9.125 -\hspace*{0pt}\\
   9.126 -\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
   9.127 -\hspace*{0pt}\\
   9.128 -\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
   9.129 -\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
   9.130 -\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
   9.131 -\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
   9.132 -\hspace*{0pt}\\
   9.133 -\hspace*{0pt}fun in{\char95}interval (k,~l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\
   9.134 -\hspace*{0pt}\\
   9.135 -\hspace*{0pt}end;~(*struct Example*)%
   9.136 +\begin{typewriter}
   9.137 +    structure\ Example\ {\isacharcolon}\ sig\isanewline
   9.138 +\ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline
   9.139 +\ \ val\ less{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline
   9.140 +\ \ val\ less{\isacharunderscore}eq{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline
   9.141 +\ \ val\ in{\isacharunderscore}interval\ {\isacharcolon}\ nat\ {\isacharasterisk}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline
   9.142 +end\ {\isacharequal}\ struct\isanewline
   9.143 +\isanewline
   9.144 +datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat{\isacharsemicolon}\isanewline
   9.145 +\isanewline
   9.146 +fun\ less{\isacharunderscore}nat\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ less{\isacharunderscore}eq{\isacharunderscore}nat\ m\ n\isanewline
   9.147 +\ \ {\isacharbar}\ less{\isacharunderscore}nat\ n\ Zero{\isacharunderscore}nat\ {\isacharequal}\ false\isanewline
   9.148 +and\ less{\isacharunderscore}eq{\isacharunderscore}nat\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n\ {\isacharequal}\ less{\isacharunderscore}nat\ m\ n\isanewline
   9.149 +\ \ {\isacharbar}\ less{\isacharunderscore}eq{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ n\ {\isacharequal}\ true{\isacharsemicolon}\isanewline
   9.150 +\isanewline
   9.151 +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
   9.152 +\isanewline
   9.153 +end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline
   9.154 +
   9.155 +  \end{typewriter}%
   9.156  \end{isamarkuptext}%
   9.157  \isamarkuptrue%
   9.158  %
    10.1 --- a/doc-src/Codegen/Thy/document/Foundations.tex	Thu Sep 23 13:28:53 2010 +0200
    10.2 +++ b/doc-src/Codegen/Thy/document/Foundations.tex	Thu Sep 23 15:46:17 2010 +0200
    10.3 @@ -245,13 +245,13 @@
    10.4  \isatagquote
    10.5  %
    10.6  \begin{isamarkuptext}%
    10.7 -\isatypewriter%
    10.8 -\noindent%
    10.9 -\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
   10.10 -\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
   10.11 -\hspace*{0pt}dequeue (AQueue xs []) =\\
   10.12 -\hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\
   10.13 -\hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));%
   10.14 +\begin{typewriter}
   10.15 +    dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Maybe\ a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline
   10.16 +dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Just\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isacharsemicolon}\isanewline
   10.17 +dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
   10.18 +\ \ {\isacharparenleft}if\ null\ xs\ then\ {\isacharparenleft}Nothing{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
   10.19 +\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}reverse\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}
   10.20 +  \end{typewriter}%
   10.21  \end{isamarkuptext}%
   10.22  \isamarkuptrue%
   10.23  %
   10.24 @@ -347,33 +347,34 @@
   10.25  \isatagquote
   10.26  %
   10.27  \begin{isamarkuptext}%
   10.28 -\isatypewriter%
   10.29 -\noindent%
   10.30 -\hspace*{0pt}structure Example :~sig\\
   10.31 -\hspace*{0pt} ~type 'a equal\\
   10.32 -\hspace*{0pt} ~val equal :~'a equal -> 'a -> 'a -> bool\\
   10.33 -\hspace*{0pt} ~val eq :~'a equal -> 'a -> 'a -> bool\\
   10.34 -\hspace*{0pt} ~val member :~'a equal -> 'a list -> 'a -> bool\\
   10.35 -\hspace*{0pt} ~val collect{\char95}duplicates :\\
   10.36 -\hspace*{0pt} ~~~'a equal -> 'a list -> 'a list -> 'a list -> 'a list\\
   10.37 -\hspace*{0pt}end = struct\\
   10.38 -\hspace*{0pt}\\
   10.39 -\hspace*{0pt}type 'a equal = {\char123}equal :~'a -> 'a -> bool{\char125};\\
   10.40 -\hspace*{0pt}val equal = {\char35}equal :~'a equal -> 'a -> 'a -> bool;\\
   10.41 -\hspace*{0pt}\\
   10.42 -\hspace*{0pt}fun eq A{\char95}~a b = equal A{\char95}~a b;\\
   10.43 -\hspace*{0pt}\\
   10.44 -\hspace*{0pt}fun member A{\char95}~[] y = false\\
   10.45 -\hspace*{0pt} ~| member A{\char95}~(x ::~xs) y = eq A{\char95}~x y orelse member A{\char95}~xs y;\\
   10.46 -\hspace*{0pt}\\
   10.47 -\hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\
   10.48 -\hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\
   10.49 -\hspace*{0pt} ~~~(if member A{\char95}~xs z\\
   10.50 -\hspace*{0pt} ~~~~~then (if member A{\char95}~ys z then collect{\char95}duplicates A{\char95}~xs ys zs\\
   10.51 -\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\
   10.52 -\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\
   10.53 -\hspace*{0pt}\\
   10.54 -\hspace*{0pt}end;~(*struct Example*)%
   10.55 +\begin{typewriter}
   10.56 +    structure\ Example\ {\isacharcolon}\ sig\isanewline
   10.57 +\ \ type\ {\isacharprime}a\ equal\isanewline
   10.58 +\ \ val\ equal\ {\isacharcolon}\ {\isacharprime}a\ equal\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ bool\isanewline
   10.59 +\ \ val\ eq\ {\isacharcolon}\ {\isacharprime}a\ equal\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ bool\isanewline
   10.60 +\ \ val\ member\ {\isacharcolon}\ {\isacharprime}a\ equal\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ bool\isanewline
   10.61 +\ \ val\ collect{\isacharunderscore}duplicates\ {\isacharcolon}\isanewline
   10.62 +\ \ \ \ {\isacharprime}a\ equal\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\isanewline
   10.63 +end\ {\isacharequal}\ struct\isanewline
   10.64 +\isanewline
   10.65 +type\ {\isacharprime}a\ equal\ {\isacharequal}\ {\isacharbraceleft}equal\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ bool{\isacharbraceright}{\isacharsemicolon}\isanewline
   10.66 +val\ equal\ {\isacharequal}\ {\isacharhash}equal\ {\isacharcolon}\ {\isacharprime}a\ equal\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ bool{\isacharsemicolon}\isanewline
   10.67 +\isanewline
   10.68 +fun\ eq\ A{\isacharunderscore}\ a\ b\ {\isacharequal}\ equal\ A{\isacharunderscore}\ a\ b{\isacharsemicolon}\isanewline
   10.69 +\isanewline
   10.70 +fun\ member\ A{\isacharunderscore}\ {\isacharbrackleft}{\isacharbrackright}\ y\ {\isacharequal}\ false\isanewline
   10.71 +\ \ {\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
   10.72 +\isanewline
   10.73 +fun\ collect{\isacharunderscore}duplicates\ A{\isacharunderscore}\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs\isanewline
   10.74 +\ \ {\isacharbar}\ collect{\isacharunderscore}duplicates\ A{\isacharunderscore}\ xs\ ys\ {\isacharparenleft}z\ {\isacharcolon}{\isacharcolon}\ zs{\isacharparenright}\ {\isacharequal}\isanewline
   10.75 +\ \ \ \ {\isacharparenleft}if\ member\ A{\isacharunderscore}\ xs\ z\isanewline
   10.76 +\ \ \ \ \ \ then\ {\isacharparenleft}if\ member\ A{\isacharunderscore}\ ys\ z\ then\ collect{\isacharunderscore}duplicates\ A{\isacharunderscore}\ xs\ ys\ zs\isanewline
   10.77 +\ \ \ \ \ \ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ A{\isacharunderscore}\ xs\ {\isacharparenleft}z\ {\isacharcolon}{\isacharcolon}\ ys{\isacharparenright}\ zs{\isacharparenright}\isanewline
   10.78 +\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ A{\isacharunderscore}\ {\isacharparenleft}z\ {\isacharcolon}{\isacharcolon}\ xs{\isacharparenright}\ {\isacharparenleft}z\ {\isacharcolon}{\isacharcolon}\ ys{\isacharparenright}\ zs{\isacharparenright}{\isacharsemicolon}\isanewline
   10.79 +\isanewline
   10.80 +end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline
   10.81 +
   10.82 +  \end{typewriter}%
   10.83  \end{isamarkuptext}%
   10.84  \isamarkuptrue%
   10.85  %
   10.86 @@ -442,14 +443,14 @@
   10.87  \isatagquote
   10.88  %
   10.89  \begin{isamarkuptext}%
   10.90 -\isatypewriter%
   10.91 -\noindent%
   10.92 -\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
   10.93 -\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
   10.94 -\hspace*{0pt} ~let {\char123}\\
   10.95 -\hspace*{0pt} ~~~(y :~ys) = reverse xs;\\
   10.96 -\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
   10.97 -\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
   10.98 +\begin{typewriter}
   10.99 +    strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline
  10.100 +strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
  10.101 +\ \ let\ {\isacharbraceleft}\isanewline
  10.102 +\ \ \ \ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}\ {\isacharequal}\ reverse\ xs{\isacharsemicolon}\isanewline
  10.103 +\ \ {\isacharbraceright}\ in\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharsemicolon}\isanewline
  10.104 +strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isacharsemicolon}
  10.105 +  \end{typewriter}%
  10.106  \end{isamarkuptext}%
  10.107  \isamarkuptrue%
  10.108  %
  10.109 @@ -533,16 +534,16 @@
  10.110  \isatagquote
  10.111  %
  10.112  \begin{isamarkuptext}%
  10.113 -\isatypewriter%
  10.114 -\noindent%
  10.115 -\hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\
  10.116 -\hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
  10.117 -\hspace*{0pt}\\
  10.118 -\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
  10.119 -\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
  10.120 -\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
  10.121 -\hspace*{0pt} ~(if null xs then empty{\char95}queue\\
  10.122 -\hspace*{0pt} ~~~else strict{\char95}dequeue (AQueue [] (reverse xs)));%
  10.123 +\begin{typewriter}
  10.124 +    empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ a{\isacharsemicolon}\isanewline
  10.125 +empty{\isacharunderscore}queue\ {\isacharequal}\ error\ {\isachardoublequote}empty{\isacharunderscore}queue{\isachardoublequote}{\isacharsemicolon}\isanewline
  10.126 +\isanewline
  10.127 +strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline
  10.128 +strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isacharsemicolon}\isanewline
  10.129 +strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
  10.130 +\ \ {\isacharparenleft}if\ null\ xs\ then\ empty{\isacharunderscore}queue\isanewline
  10.131 +\ \ \ \ else\ strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}reverse\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}
  10.132 +  \end{typewriter}%
  10.133  \end{isamarkuptext}%
  10.134  \isamarkuptrue%
  10.135  %
    11.1 --- a/doc-src/Codegen/Thy/document/Further.tex	Thu Sep 23 13:28:53 2010 +0200
    11.2 +++ b/doc-src/Codegen/Thy/document/Further.tex	Thu Sep 23 15:46:17 2010 +0200
    11.3 @@ -214,15 +214,15 @@
    11.4  \isatagquote
    11.5  %
    11.6  \begin{isamarkuptext}%
    11.7 -\isatypewriter%
    11.8 -\noindent%
    11.9 -\hspace*{0pt}funpow ::~forall a.~Nat -> (a -> a) -> a -> a;\\
   11.10 -\hspace*{0pt}funpow Zero{\char95}nat f = id;\\
   11.11 -\hspace*{0pt}funpow (Suc n) f = f .~funpow n f;\\
   11.12 -\hspace*{0pt}\\
   11.13 -\hspace*{0pt}funpows ::~forall a.~[Nat] -> (a -> a) -> a -> a;\\
   11.14 -\hspace*{0pt}funpows [] = id;\\
   11.15 -\hspace*{0pt}funpows (x :~xs) = funpow x .~funpows xs;%
   11.16 +\begin{typewriter}
   11.17 +    funpow\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Nat\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a\ {\isacharminus}{\isachargreater}\ a{\isacharparenright}\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
   11.18 +funpow\ Zero{\isacharunderscore}nat\ f\ {\isacharequal}\ id{\isacharsemicolon}\isanewline
   11.19 +funpow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ f\ {\isacharequal}\ f\ {\isachardot}\ funpow\ n\ f{\isacharsemicolon}\isanewline
   11.20 +\isanewline
   11.21 +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
   11.22 +funpows\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ id{\isacharsemicolon}\isanewline
   11.23 +funpows\ {\isacharparenleft}x\ {\isacharcolon}\ xs{\isacharparenright}\ {\isacharequal}\ funpow\ x\ {\isachardot}\ funpows\ xs{\isacharsemicolon}
   11.24 +  \end{typewriter}%
   11.25  \end{isamarkuptext}%
   11.26  \isamarkuptrue%
   11.27  %
    12.1 --- a/doc-src/Codegen/Thy/document/Introduction.tex	Thu Sep 23 13:28:53 2010 +0200
    12.2 +++ b/doc-src/Codegen/Thy/document/Introduction.tex	Thu Sep 23 15:46:17 2010 +0200
    12.3 @@ -140,41 +140,42 @@
    12.4  \isatagquote
    12.5  %
    12.6  \begin{isamarkuptext}%
    12.7 -\isatypewriter%
    12.8 -\noindent%
    12.9 -\hspace*{0pt}structure Example :~sig\\
   12.10 -\hspace*{0pt} ~val id :~'a -> 'a\\
   12.11 -\hspace*{0pt} ~val fold :~('a -> 'b -> 'b) -> 'a list -> 'b -> 'b\\
   12.12 -\hspace*{0pt} ~val rev :~'a list -> 'a list\\
   12.13 -\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
   12.14 -\hspace*{0pt} ~val empty :~'a queue\\
   12.15 -\hspace*{0pt} ~val dequeue :~'a queue -> 'a option * 'a queue\\
   12.16 -\hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
   12.17 -\hspace*{0pt}end = struct\\
   12.18 -\hspace*{0pt}\\
   12.19 -\hspace*{0pt}fun id x = (fn xa => xa) x;\\
   12.20 -\hspace*{0pt}\\
   12.21 -\hspace*{0pt}fun fold f [] = id\\
   12.22 -\hspace*{0pt} ~| fold f (x ::~xs) = fold f xs o f x;\\
   12.23 -\hspace*{0pt}\\
   12.24 -\hspace*{0pt}fun rev xs = fold (fn a => fn b => a ::~b) xs [];\\
   12.25 -\hspace*{0pt}\\
   12.26 -\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
   12.27 -\hspace*{0pt}\\
   12.28 -\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\
   12.29 -\hspace*{0pt}\\
   12.30 -\hspace*{0pt}fun dequeue (AQueue ([],~[])) = (NONE,~AQueue ([],~[]))\\
   12.31 -\hspace*{0pt} ~| dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
   12.32 -\hspace*{0pt} ~| dequeue (AQueue (v ::~va,~[])) =\\
   12.33 -\hspace*{0pt} ~~~let\\
   12.34 -\hspace*{0pt} ~~~~~val y ::~ys = rev (v ::~va);\\
   12.35 -\hspace*{0pt} ~~~in\\
   12.36 -\hspace*{0pt} ~~~~~(SOME y,~AQueue ([],~ys))\\
   12.37 -\hspace*{0pt} ~~~end;\\
   12.38 -\hspace*{0pt}\\
   12.39 -\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
   12.40 -\hspace*{0pt}\\
   12.41 -\hspace*{0pt}end;~(*struct Example*)%
   12.42 +\begin{typewriter}
   12.43 +    structure\ Example\ {\isacharcolon}\ sig\isanewline
   12.44 +\ \ val\ id\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
   12.45 +\ \ 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
   12.46 +\ \ val\ rev\ {\isacharcolon}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\isanewline
   12.47 +\ \ datatype\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ of\ {\isacharprime}a\ list\ {\isacharasterisk}\ {\isacharprime}a\ list\isanewline
   12.48 +\ \ val\ empty\ {\isacharcolon}\ {\isacharprime}a\ queue\isanewline
   12.49 +\ \ val\ dequeue\ {\isacharcolon}\ {\isacharprime}a\ queue\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ option\ {\isacharasterisk}\ {\isacharprime}a\ queue\isanewline
   12.50 +\ \ val\ enqueue\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ queue\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ queue\isanewline
   12.51 +end\ {\isacharequal}\ struct\isanewline
   12.52 +\isanewline
   12.53 +fun\ id\ x\ {\isacharequal}\ {\isacharparenleft}fn\ xa\ {\isacharequal}{\isachargreater}\ xa{\isacharparenright}\ x{\isacharsemicolon}\isanewline
   12.54 +\isanewline
   12.55 +fun\ fold\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ id\isanewline
   12.56 +\ \ {\isacharbar}\ fold\ f\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharparenright}\ {\isacharequal}\ fold\ f\ xs\ o\ f\ x{\isacharsemicolon}\isanewline
   12.57 +\isanewline
   12.58 +fun\ rev\ xs\ {\isacharequal}\ fold\ {\isacharparenleft}fn\ a\ {\isacharequal}{\isachargreater}\ fn\ b\ {\isacharequal}{\isachargreater}\ a\ {\isacharcolon}{\isacharcolon}\ b{\isacharparenright}\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline
   12.59 +\isanewline
   12.60 +datatype\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ of\ {\isacharprime}a\ list\ {\isacharasterisk}\ {\isacharprime}a\ list{\isacharsemicolon}\isanewline
   12.61 +\isanewline
   12.62 +val\ empty\ {\isacharcolon}\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharsemicolon}\isanewline
   12.63 +\isanewline
   12.64 +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
   12.65 +\ \ {\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
   12.66 +\ \ {\isacharbar}\ dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}v\ {\isacharcolon}{\isacharcolon}\ va{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
   12.67 +\ \ \ \ let\isanewline
   12.68 +\ \ \ \ \ \ val\ y\ {\isacharcolon}{\isacharcolon}\ ys\ {\isacharequal}\ rev\ {\isacharparenleft}v\ {\isacharcolon}{\isacharcolon}\ va{\isacharparenright}{\isacharsemicolon}\isanewline
   12.69 +\ \ \ \ in\isanewline
   12.70 +\ \ \ \ \ \ {\isacharparenleft}SOME\ y{\isacharcomma}\ AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ ys{\isacharparenright}{\isacharparenright}\isanewline
   12.71 +\ \ \ \ end{\isacharsemicolon}\isanewline
   12.72 +\isanewline
   12.73 +fun\ enqueue\ x\ {\isacharparenleft}AQueue\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharcomma}\ ys{\isacharparenright}{\isacharsemicolon}\isanewline
   12.74 +\isanewline
   12.75 +end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline
   12.76 +
   12.77 +  \end{typewriter}%
   12.78  \end{isamarkuptext}%
   12.79  \isamarkuptrue%
   12.80  %
   12.81 @@ -225,27 +226,28 @@
   12.82  \isatagquote
   12.83  %
   12.84  \begin{isamarkuptext}%
   12.85 -\isatypewriter%
   12.86 -\noindent%
   12.87 -\hspace*{0pt}module Example where {\char123}\\
   12.88 -\hspace*{0pt}\\
   12.89 -\hspace*{0pt}data Queue a = AQueue [a] [a];\\
   12.90 -\hspace*{0pt}\\
   12.91 -\hspace*{0pt}empty ::~forall a.~Queue a;\\
   12.92 -\hspace*{0pt}empty = AQueue [] [];\\
   12.93 -\hspace*{0pt}\\
   12.94 -\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
   12.95 -\hspace*{0pt}dequeue (AQueue [] []) = (Nothing,~AQueue [] []);\\
   12.96 -\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
   12.97 -\hspace*{0pt}dequeue (AQueue (v :~va) []) =\\
   12.98 -\hspace*{0pt} ~let {\char123}\\
   12.99 -\hspace*{0pt} ~~~(y :~ys) = reverse (v :~va);\\
  12.100 -\hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys);\\
  12.101 -\hspace*{0pt}\\
  12.102 -\hspace*{0pt}enqueue ::~forall a.~a -> Queue a -> Queue a;\\
  12.103 -\hspace*{0pt}enqueue x (AQueue xs ys) = AQueue (x :~xs) ys;\\
  12.104 -\hspace*{0pt}\\
  12.105 -\hspace*{0pt}{\char125}%
  12.106 +\begin{typewriter}
  12.107 +    module\ Example\ where\ {\isacharbraceleft}\isanewline
  12.108 +\isanewline
  12.109 +data\ Queue\ a\ {\isacharequal}\ AQueue\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharbrackleft}a{\isacharbrackright}{\isacharsemicolon}\isanewline
  12.110 +\isanewline
  12.111 +empty\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a{\isacharsemicolon}\isanewline
  12.112 +empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline
  12.113 +\isanewline
  12.114 +dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Maybe\ a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline
  12.115 +dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Nothing{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharsemicolon}\isanewline
  12.116 +dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Just\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isacharsemicolon}\isanewline
  12.117 +dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}v\ {\isacharcolon}\ va{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
  12.118 +\ \ let\ {\isacharbraceleft}\isanewline
  12.119 +\ \ \ \ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}\ {\isacharequal}\ reverse\ {\isacharparenleft}v\ {\isacharcolon}\ va{\isacharparenright}{\isacharsemicolon}\isanewline
  12.120 +\ \ {\isacharbraceright}\ in\ {\isacharparenleft}Just\ y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharsemicolon}\isanewline
  12.121 +\isanewline
  12.122 +enqueue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ a\ {\isacharminus}{\isachargreater}\ Queue\ a\ {\isacharminus}{\isachargreater}\ Queue\ a{\isacharsemicolon}\isanewline
  12.123 +enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharcolon}\ xs{\isacharparenright}\ ys{\isacharsemicolon}\isanewline
  12.124 +\isanewline
  12.125 +{\isacharbraceright}\isanewline
  12.126 +
  12.127 +  \end{typewriter}%
  12.128  \end{isamarkuptext}%
  12.129  \isamarkuptrue%
  12.130  %
  12.131 @@ -393,47 +395,48 @@
  12.132  \isatagquote
  12.133  %
  12.134  \begin{isamarkuptext}%
  12.135 -\isatypewriter%
  12.136 -\noindent%
  12.137 -\hspace*{0pt}module Example where {\char123}\\
  12.138 -\hspace*{0pt}\\
  12.139 -\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
  12.140 -\hspace*{0pt}\\
  12.141 -\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\
  12.142 -\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\
  12.143 -\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\
  12.144 -\hspace*{0pt}\\
  12.145 -\hspace*{0pt}class Semigroup a where {\char123}\\
  12.146 -\hspace*{0pt} ~mult ::~a -> a -> a;\\
  12.147 -\hspace*{0pt}{\char125};\\
  12.148 -\hspace*{0pt}\\
  12.149 -\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\
  12.150 -\hspace*{0pt} ~neutral ::~a;\\
  12.151 -\hspace*{0pt}{\char125};\\
  12.152 -\hspace*{0pt}\\
  12.153 -\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\
  12.154 -\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\
  12.155 -\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\
  12.156 -\hspace*{0pt}\\
  12.157 -\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\
  12.158 -\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\
  12.159 -\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
  12.160 -\hspace*{0pt}\\
  12.161 -\hspace*{0pt}instance Semigroup Nat where {\char123}\\
  12.162 -\hspace*{0pt} ~mult = mult{\char95}nat;\\
  12.163 -\hspace*{0pt}{\char125};\\
  12.164 -\hspace*{0pt}\\
  12.165 -\hspace*{0pt}neutral{\char95}nat ::~Nat;\\
  12.166 -\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\
  12.167 -\hspace*{0pt}\\
  12.168 -\hspace*{0pt}instance Monoid Nat where {\char123}\\
  12.169 -\hspace*{0pt} ~neutral = neutral{\char95}nat;\\
  12.170 -\hspace*{0pt}{\char125};\\
  12.171 -\hspace*{0pt}\\
  12.172 -\hspace*{0pt}bexp ::~Nat -> Nat;\\
  12.173 -\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\
  12.174 -\hspace*{0pt}\\
  12.175 -\hspace*{0pt}{\char125}%
  12.176 +\begin{typewriter}
  12.177 +    module\ Example\ where\ {\isacharbraceleft}\isanewline
  12.178 +\isanewline
  12.179 +data\ Nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ Nat{\isacharsemicolon}\isanewline
  12.180 +\isanewline
  12.181 +plus{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
  12.182 +plus{\isacharunderscore}nat\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n\ {\isacharequal}\ plus{\isacharunderscore}nat\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharsemicolon}\isanewline
  12.183 +plus{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ n\ {\isacharequal}\ n{\isacharsemicolon}\isanewline
  12.184 +\isanewline
  12.185 +class\ Semigroup\ a\ where\ {\isacharbraceleft}\isanewline
  12.186 +\ \ mult\ {\isacharcolon}{\isacharcolon}\ a\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
  12.187 +{\isacharbraceright}{\isacharsemicolon}\isanewline
  12.188 +\isanewline
  12.189 +class\ {\isacharparenleft}Semigroup\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Monoid\ a\ where\ {\isacharbraceleft}\isanewline
  12.190 +\ \ neutral\ {\isacharcolon}{\isacharcolon}\ a{\isacharsemicolon}\isanewline
  12.191 +{\isacharbraceright}{\isacharsemicolon}\isanewline
  12.192 +\isanewline
  12.193 +pow\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Monoid\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Nat\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
  12.194 +pow\ Zero{\isacharunderscore}nat\ a\ {\isacharequal}\ neutral{\isacharsemicolon}\isanewline
  12.195 +pow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ mult\ a\ {\isacharparenleft}pow\ n\ a{\isacharparenright}{\isacharsemicolon}\isanewline
  12.196 +\isanewline
  12.197 +mult{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
  12.198 +mult{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ n\ {\isacharequal}\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline
  12.199 +mult{\isacharunderscore}nat\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n\ {\isacharequal}\ plus{\isacharunderscore}nat\ n\ {\isacharparenleft}mult{\isacharunderscore}nat\ m\ n{\isacharparenright}{\isacharsemicolon}\isanewline
  12.200 +\isanewline
  12.201 +instance\ Semigroup\ Nat\ where\ {\isacharbraceleft}\isanewline
  12.202 +\ \ mult\ {\isacharequal}\ mult{\isacharunderscore}nat{\isacharsemicolon}\isanewline
  12.203 +{\isacharbraceright}{\isacharsemicolon}\isanewline
  12.204 +\isanewline
  12.205 +neutral{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ Nat{\isacharsemicolon}\isanewline
  12.206 +neutral{\isacharunderscore}nat\ {\isacharequal}\ Suc\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline
  12.207 +\isanewline
  12.208 +instance\ Monoid\ Nat\ where\ {\isacharbraceleft}\isanewline
  12.209 +\ \ neutral\ {\isacharequal}\ neutral{\isacharunderscore}nat{\isacharsemicolon}\isanewline
  12.210 +{\isacharbraceright}{\isacharsemicolon}\isanewline
  12.211 +\isanewline
  12.212 +bexp\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
  12.213 +bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ Zero{\isacharunderscore}nat{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
  12.214 +\isanewline
  12.215 +{\isacharbraceright}\isanewline
  12.216 +
  12.217 +  \end{typewriter}%
  12.218  \end{isamarkuptext}%
  12.219  \isamarkuptrue%
  12.220  %
  12.221 @@ -458,52 +461,53 @@
  12.222  \isatagquote
  12.223  %
  12.224  \begin{isamarkuptext}%
  12.225 -\isatypewriter%
  12.226 -\noindent%
  12.227 -\hspace*{0pt}structure Example :~sig\\
  12.228 -\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
  12.229 -\hspace*{0pt} ~val plus{\char95}nat :~nat -> nat -> nat\\
  12.230 -\hspace*{0pt} ~type 'a semigroup\\
  12.231 -\hspace*{0pt} ~val mult :~'a semigroup -> 'a -> 'a -> 'a\\
  12.232 -\hspace*{0pt} ~type 'a monoid\\
  12.233 -\hspace*{0pt} ~val semigroup{\char95}monoid :~'a monoid -> 'a semigroup\\
  12.234 -\hspace*{0pt} ~val neutral :~'a monoid -> 'a\\
  12.235 -\hspace*{0pt} ~val pow :~'a monoid -> nat -> 'a -> 'a\\
  12.236 -\hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\
  12.237 -\hspace*{0pt} ~val semigroup{\char95}nat :~nat semigroup\\
  12.238 -\hspace*{0pt} ~val neutral{\char95}nat :~nat\\
  12.239 -\hspace*{0pt} ~val monoid{\char95}nat :~nat monoid\\
  12.240 -\hspace*{0pt} ~val bexp :~nat -> nat\\
  12.241 -\hspace*{0pt}end = struct\\
  12.242 -\hspace*{0pt}\\
  12.243 -\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
  12.244 -\hspace*{0pt}\\
  12.245 -\hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\
  12.246 -\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
  12.247 -\hspace*{0pt}\\
  12.248 -\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
  12.249 -\hspace*{0pt}val mult = {\char35}mult :~'a semigroup -> 'a -> 'a -> 'a;\\
  12.250 -\hspace*{0pt}\\
  12.251 -\hspace*{0pt}type 'a monoid = {\char123}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\
  12.252 -\hspace*{0pt}val semigroup{\char95}monoid = {\char35}semigroup{\char95}monoid :~'a monoid -> 'a semigroup;\\
  12.253 -\hspace*{0pt}val neutral = {\char35}neutral :~'a monoid -> 'a;\\
  12.254 -\hspace*{0pt}\\
  12.255 -\hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\
  12.256 -\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\
  12.257 -\hspace*{0pt}\\
  12.258 -\hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\
  12.259 -\hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
  12.260 -\hspace*{0pt}\\
  12.261 -\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\
  12.262 -\hspace*{0pt}\\
  12.263 -\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\
  12.264 -\hspace*{0pt}\\
  12.265 -\hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\
  12.266 -\hspace*{0pt} ~:~nat monoid;\\
  12.267 -\hspace*{0pt}\\
  12.268 -\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\
  12.269 -\hspace*{0pt}\\
  12.270 -\hspace*{0pt}end;~(*struct Example*)%
  12.271 +\begin{typewriter}
  12.272 +    structure\ Example\ {\isacharcolon}\ sig\isanewline
  12.273 +\ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline
  12.274 +\ \ val\ plus{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ nat\isanewline
  12.275 +\ \ type\ {\isacharprime}a\ semigroup\isanewline
  12.276 +\ \ val\ mult\ {\isacharcolon}\ {\isacharprime}a\ semigroup\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
  12.277 +\ \ type\ {\isacharprime}a\ monoid\isanewline
  12.278 +\ \ val\ semigroup{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ semigroup\isanewline
  12.279 +\ \ val\ neutral\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
  12.280 +\ \ val\ pow\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
  12.281 +\ \ val\ mult{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ nat\isanewline
  12.282 +\ \ val\ semigroup{\isacharunderscore}nat\ {\isacharcolon}\ nat\ semigroup\isanewline
  12.283 +\ \ val\ neutral{\isacharunderscore}nat\ {\isacharcolon}\ nat\isanewline
  12.284 +\ \ val\ monoid{\isacharunderscore}nat\ {\isacharcolon}\ nat\ monoid\isanewline
  12.285 +\ \ val\ bexp\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\isanewline
  12.286 +end\ {\isacharequal}\ struct\isanewline
  12.287 +\isanewline
  12.288 +datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat{\isacharsemicolon}\isanewline
  12.289 +\isanewline
  12.290 +fun\ plus{\isacharunderscore}nat\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n\ {\isacharequal}\ plus{\isacharunderscore}nat\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}\isanewline
  12.291 +\ \ {\isacharbar}\ plus{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ n\ {\isacharequal}\ n{\isacharsemicolon}\isanewline
  12.292 +\isanewline
  12.293 +type\ {\isacharprime}a\ semigroup\ {\isacharequal}\ {\isacharbraceleft}mult\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharbraceright}{\isacharsemicolon}\isanewline
  12.294 +val\ mult\ {\isacharequal}\ {\isacharhash}mult\ {\isacharcolon}\ {\isacharprime}a\ semigroup\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharsemicolon}\isanewline
  12.295 +\isanewline
  12.296 +type\ {\isacharprime}a\ monoid\ {\isacharequal}\ {\isacharbraceleft}semigroup{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ semigroup{\isacharcomma}\ neutral\ {\isacharcolon}\ {\isacharprime}a{\isacharbraceright}{\isacharsemicolon}\isanewline
  12.297 +val\ semigroup{\isacharunderscore}monoid\ {\isacharequal}\ {\isacharhash}semigroup{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ semigroup{\isacharsemicolon}\isanewline
  12.298 +val\ neutral\ {\isacharequal}\ {\isacharhash}neutral\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharsemicolon}\isanewline
  12.299 +\isanewline
  12.300 +fun\ pow\ A{\isacharunderscore}\ Zero{\isacharunderscore}nat\ a\ {\isacharequal}\ neutral\ A{\isacharunderscore}\isanewline
  12.301 +\ \ {\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
  12.302 +\isanewline
  12.303 +fun\ mult{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ n\ {\isacharequal}\ Zero{\isacharunderscore}nat\isanewline
  12.304 +\ \ {\isacharbar}\ mult{\isacharunderscore}nat\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n\ {\isacharequal}\ plus{\isacharunderscore}nat\ n\ {\isacharparenleft}mult{\isacharunderscore}nat\ m\ n{\isacharparenright}{\isacharsemicolon}\isanewline
  12.305 +\isanewline
  12.306 +val\ semigroup{\isacharunderscore}nat\ {\isacharequal}\ {\isacharbraceleft}mult\ {\isacharequal}\ mult{\isacharunderscore}nat{\isacharbraceright}\ {\isacharcolon}\ nat\ semigroup{\isacharsemicolon}\isanewline
  12.307 +\isanewline
  12.308 +val\ neutral{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharequal}\ Suc\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline
  12.309 +\isanewline
  12.310 +val\ monoid{\isacharunderscore}nat\ {\isacharequal}\ {\isacharbraceleft}semigroup{\isacharunderscore}monoid\ {\isacharequal}\ semigroup{\isacharunderscore}nat{\isacharcomma}\ neutral\ {\isacharequal}\ neutral{\isacharunderscore}nat{\isacharbraceright}\isanewline
  12.311 +\ \ {\isacharcolon}\ nat\ monoid{\isacharsemicolon}\isanewline
  12.312 +\isanewline
  12.313 +fun\ bexp\ n\ {\isacharequal}\ pow\ monoid{\isacharunderscore}nat\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ Zero{\isacharunderscore}nat{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
  12.314 +\isanewline
  12.315 +end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline
  12.316 +
  12.317 +  \end{typewriter}%
  12.318  \end{isamarkuptext}%
  12.319  \isamarkuptrue%
  12.320  %
    13.1 --- a/doc-src/Codegen/Thy/document/Refinement.tex	Thu Sep 23 13:28:53 2010 +0200
    13.2 +++ b/doc-src/Codegen/Thy/document/Refinement.tex	Thu Sep 23 15:46:17 2010 +0200
    13.3 @@ -72,12 +72,12 @@
    13.4  \isatagquote
    13.5  %
    13.6  \begin{isamarkuptext}%
    13.7 -\isatypewriter%
    13.8 -\noindent%
    13.9 -\hspace*{0pt}fib ::~Nat -> Nat;\\
   13.10 -\hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;\\
   13.11 -\hspace*{0pt}fib (Suc Zero{\char95}nat) = Suc Zero{\char95}nat;\\
   13.12 -\hspace*{0pt}fib (Suc (Suc n)) = plus{\char95}nat (fib n) (fib (Suc n));%
   13.13 +\begin{typewriter}
   13.14 +    fib\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
   13.15 +fib\ Zero{\isacharunderscore}nat\ {\isacharequal}\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline
   13.16 +fib\ {\isacharparenleft}Suc\ Zero{\isacharunderscore}nat{\isacharparenright}\ {\isacharequal}\ Suc\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline
   13.17 +fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ plus{\isacharunderscore}nat\ {\isacharparenleft}fib\ n{\isacharparenright}\ {\isacharparenleft}fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isacharsemicolon}
   13.18 +  \end{typewriter}%
   13.19  \end{isamarkuptext}%
   13.20  \isamarkuptrue%
   13.21  %
   13.22 @@ -170,17 +170,17 @@
   13.23  \isatagquote
   13.24  %
   13.25  \begin{isamarkuptext}%
   13.26 -\isatypewriter%
   13.27 -\noindent%
   13.28 -\hspace*{0pt}fib{\char95}step ::~Nat -> (Nat,~Nat);\\
   13.29 -\hspace*{0pt}fib{\char95}step (Suc n) = let {\char123}\\
   13.30 -\hspace*{0pt} ~~~~~~~~~~~~~~~~~~~~(m,~q) = fib{\char95}step n;\\
   13.31 -\hspace*{0pt} ~~~~~~~~~~~~~~~~~~{\char125}~in (plus{\char95}nat m q,~m);\\
   13.32 -\hspace*{0pt}fib{\char95}step Zero{\char95}nat = (Suc Zero{\char95}nat,~Zero{\char95}nat);\\
   13.33 -\hspace*{0pt}\\
   13.34 -\hspace*{0pt}fib ::~Nat -> Nat;\\
   13.35 -\hspace*{0pt}fib (Suc n) = fst (fib{\char95}step n);\\
   13.36 -\hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;%
   13.37 +\begin{typewriter}
   13.38 +    fib{\isacharunderscore}step\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Nat{\isacharcomma}\ Nat{\isacharparenright}{\isacharsemicolon}\isanewline
   13.39 +fib{\isacharunderscore}step\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ let\ {\isacharbraceleft}\isanewline
   13.40 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}m{\isacharcomma}\ q{\isacharparenright}\ {\isacharequal}\ fib{\isacharunderscore}step\ n{\isacharsemicolon}\isanewline
   13.41 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbraceright}\ in\ {\isacharparenleft}plus{\isacharunderscore}nat\ m\ q{\isacharcomma}\ m{\isacharparenright}{\isacharsemicolon}\isanewline
   13.42 +fib{\isacharunderscore}step\ Zero{\isacharunderscore}nat\ {\isacharequal}\ {\isacharparenleft}Suc\ Zero{\isacharunderscore}nat{\isacharcomma}\ Zero{\isacharunderscore}nat{\isacharparenright}{\isacharsemicolon}\isanewline
   13.43 +\isanewline
   13.44 +fib\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
   13.45 +fib\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ fst\ {\isacharparenleft}fib{\isacharunderscore}step\ n{\isacharparenright}{\isacharsemicolon}\isanewline
   13.46 +fib\ Zero{\isacharunderscore}nat\ {\isacharequal}\ Zero{\isacharunderscore}nat{\isacharsemicolon}
   13.47 +  \end{typewriter}%
   13.48  \end{isamarkuptext}%
   13.49  \isamarkuptrue%
   13.50  %
   13.51 @@ -348,41 +348,42 @@
   13.52  \isatagquote
   13.53  %
   13.54  \begin{isamarkuptext}%
   13.55 -\isatypewriter%
   13.56 -\noindent%
   13.57 -\hspace*{0pt}structure Example :~sig\\
   13.58 -\hspace*{0pt} ~val id :~'a -> 'a\\
   13.59 -\hspace*{0pt} ~val fold :~('a -> 'b -> 'b) -> 'a list -> 'b -> 'b\\
   13.60 -\hspace*{0pt} ~val rev :~'a list -> 'a list\\
   13.61 -\hspace*{0pt} ~val null :~'a list -> bool\\
   13.62 -\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
   13.63 -\hspace*{0pt} ~val empty :~'a queue\\
   13.64 -\hspace*{0pt} ~val dequeue :~'a queue -> 'a option * 'a queue\\
   13.65 -\hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
   13.66 -\hspace*{0pt}end = struct\\
   13.67 -\hspace*{0pt}\\
   13.68 -\hspace*{0pt}fun id x = (fn xa => xa) x;\\
   13.69 -\hspace*{0pt}\\
   13.70 -\hspace*{0pt}fun fold f [] = id\\
   13.71 -\hspace*{0pt} ~| fold f (x ::~xs) = fold f xs o f x;\\
   13.72 -\hspace*{0pt}\\
   13.73 -\hspace*{0pt}fun rev xs = fold (fn a => fn b => a ::~b) xs [];\\
   13.74 -\hspace*{0pt}\\
   13.75 -\hspace*{0pt}fun null [] = true\\
   13.76 -\hspace*{0pt} ~| null (x ::~xs) = false;\\
   13.77 -\hspace*{0pt}\\
   13.78 -\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
   13.79 -\hspace*{0pt}\\
   13.80 -\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\
   13.81 -\hspace*{0pt}\\
   13.82 -\hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
   13.83 -\hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\
   13.84 -\hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\
   13.85 -\hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\
   13.86 -\hspace*{0pt}\\
   13.87 -\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
   13.88 -\hspace*{0pt}\\
   13.89 -\hspace*{0pt}end;~(*struct Example*)%
   13.90 +\begin{typewriter}
   13.91 +    structure\ Example\ {\isacharcolon}\ sig\isanewline
   13.92 +\ \ val\ id\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
   13.93 +\ \ 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
   13.94 +\ \ val\ rev\ {\isacharcolon}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\isanewline
   13.95 +\ \ val\ null\ {\isacharcolon}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ bool\isanewline
   13.96 +\ \ datatype\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ of\ {\isacharprime}a\ list\ {\isacharasterisk}\ {\isacharprime}a\ list\isanewline
   13.97 +\ \ val\ empty\ {\isacharcolon}\ {\isacharprime}a\ queue\isanewline
   13.98 +\ \ val\ dequeue\ {\isacharcolon}\ {\isacharprime}a\ queue\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ option\ {\isacharasterisk}\ {\isacharprime}a\ queue\isanewline
   13.99 +\ \ val\ enqueue\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ queue\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ queue\isanewline
  13.100 +end\ {\isacharequal}\ struct\isanewline
  13.101 +\isanewline
  13.102 +fun\ id\ x\ {\isacharequal}\ {\isacharparenleft}fn\ xa\ {\isacharequal}{\isachargreater}\ xa{\isacharparenright}\ x{\isacharsemicolon}\isanewline
  13.103 +\isanewline
  13.104 +fun\ fold\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ id\isanewline
  13.105 +\ \ {\isacharbar}\ fold\ f\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharparenright}\ {\isacharequal}\ fold\ f\ xs\ o\ f\ x{\isacharsemicolon}\isanewline
  13.106 +\isanewline
  13.107 +fun\ rev\ xs\ {\isacharequal}\ fold\ {\isacharparenleft}fn\ a\ {\isacharequal}{\isachargreater}\ fn\ b\ {\isacharequal}{\isachargreater}\ a\ {\isacharcolon}{\isacharcolon}\ b{\isacharparenright}\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline
  13.108 +\isanewline
  13.109 +fun\ null\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ true\isanewline
  13.110 +\ \ {\isacharbar}\ null\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharparenright}\ {\isacharequal}\ false{\isacharsemicolon}\isanewline
  13.111 +\isanewline
  13.112 +datatype\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ of\ {\isacharprime}a\ list\ {\isacharasterisk}\ {\isacharprime}a\ list{\isacharsemicolon}\isanewline
  13.113 +\isanewline
  13.114 +val\ empty\ {\isacharcolon}\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharsemicolon}\isanewline
  13.115 +\isanewline
  13.116 +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
  13.117 +\ \ {\isacharbar}\ dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}xs{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
  13.118 +\ \ \ \ {\isacharparenleft}if\ null\ xs\ then\ {\isacharparenleft}NONE{\isacharcomma}\ AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
  13.119 +\ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
  13.120 +\isanewline
  13.121 +fun\ enqueue\ x\ {\isacharparenleft}AQueue\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharcomma}\ ys{\isacharparenright}{\isacharsemicolon}\isanewline
  13.122 +\isanewline
  13.123 +end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline
  13.124 +
  13.125 +  \end{typewriter}%
  13.126  \end{isamarkuptext}%
  13.127  \isamarkuptrue%
  13.128  %
  13.129 @@ -584,36 +585,37 @@
  13.130  \isatagquote
  13.131  %
  13.132  \begin{isamarkuptext}%
  13.133 -\isatypewriter%
  13.134 -\noindent%
  13.135 -\hspace*{0pt}module Example where {\char123}\\
  13.136 -\hspace*{0pt}\\
  13.137 -\hspace*{0pt}newtype Dlist a = Dlist [a];\\
  13.138 -\hspace*{0pt}\\
  13.139 -\hspace*{0pt}empty ::~forall a.~Dlist a;\\
  13.140 -\hspace*{0pt}empty = Dlist [];\\
  13.141 -\hspace*{0pt}\\
  13.142 -\hspace*{0pt}member ::~forall a.~(Eq a) => [a] -> a -> Bool;\\
  13.143 -\hspace*{0pt}member [] y = False;\\
  13.144 -\hspace*{0pt}member (x :~xs) y = x == y || member xs y;\\
  13.145 -\hspace*{0pt}\\
  13.146 -\hspace*{0pt}insert ::~forall a.~(Eq a) => a -> [a] -> [a];\\
  13.147 -\hspace*{0pt}insert x xs = (if member xs x then xs else x :~xs);\\
  13.148 -\hspace*{0pt}\\
  13.149 -\hspace*{0pt}list{\char95}of{\char95}dlist ::~forall a.~Dlist a -> [a];\\
  13.150 -\hspace*{0pt}list{\char95}of{\char95}dlist (Dlist x) = x;\\
  13.151 -\hspace*{0pt}\\
  13.152 -\hspace*{0pt}inserta ::~forall a.~(Eq a) => a -> Dlist a -> Dlist a;\\
  13.153 -\hspace*{0pt}inserta x dxs = Dlist (insert x (list{\char95}of{\char95}dlist dxs));\\
  13.154 -\hspace*{0pt}\\
  13.155 -\hspace*{0pt}remove1 ::~forall a.~(Eq a) => a -> [a] -> [a];\\
  13.156 -\hspace*{0pt}remove1 x [] = [];\\
  13.157 -\hspace*{0pt}remove1 x (y :~xs) = (if x == y then xs else y :~remove1 x xs);\\
  13.158 -\hspace*{0pt}\\
  13.159 -\hspace*{0pt}remove ::~forall a.~(Eq a) => a -> Dlist a -> Dlist a;\\
  13.160 -\hspace*{0pt}remove x dxs = Dlist (remove1 x (list{\char95}of{\char95}dlist dxs));\\
  13.161 -\hspace*{0pt}\\
  13.162 -\hspace*{0pt}{\char125}%
  13.163 +\begin{typewriter}
  13.164 +    module\ Example\ where\ {\isacharbraceleft}\isanewline
  13.165 +\isanewline
  13.166 +newtype\ Dlist\ a\ {\isacharequal}\ Dlist\ {\isacharbrackleft}a{\isacharbrackright}{\isacharsemicolon}\isanewline
  13.167 +\isanewline
  13.168 +empty\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Dlist\ a{\isacharsemicolon}\isanewline
  13.169 +empty\ {\isacharequal}\ Dlist\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline
  13.170 +\isanewline
  13.171 +member\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Eq\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ Bool{\isacharsemicolon}\isanewline
  13.172 +member\ {\isacharbrackleft}{\isacharbrackright}\ y\ {\isacharequal}\ False{\isacharsemicolon}\isanewline
  13.173 +member\ {\isacharparenleft}x\ {\isacharcolon}\ xs{\isacharparenright}\ y\ {\isacharequal}\ x\ {\isacharequal}{\isacharequal}\ y\ {\isacharbar}{\isacharbar}\ member\ xs\ y{\isacharsemicolon}\isanewline
  13.174 +\isanewline
  13.175 +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
  13.176 +insert\ x\ xs\ {\isacharequal}\ {\isacharparenleft}if\ member\ xs\ x\ then\ xs\ else\ x\ {\isacharcolon}\ xs{\isacharparenright}{\isacharsemicolon}\isanewline
  13.177 +\isanewline
  13.178 +list{\isacharunderscore}of{\isacharunderscore}dlist\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Dlist\ a\ {\isacharminus}{\isachargreater}\ {\isacharbrackleft}a{\isacharbrackright}{\isacharsemicolon}\isanewline
  13.179 +list{\isacharunderscore}of{\isacharunderscore}dlist\ {\isacharparenleft}Dlist\ x{\isacharparenright}\ {\isacharequal}\ x{\isacharsemicolon}\isanewline
  13.180 +\isanewline
  13.181 +inserta\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Eq\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ Dlist\ a\ {\isacharminus}{\isachargreater}\ Dlist\ a{\isacharsemicolon}\isanewline
  13.182 +inserta\ x\ dxs\ {\isacharequal}\ Dlist\ {\isacharparenleft}insert\ x\ {\isacharparenleft}list{\isacharunderscore}of{\isacharunderscore}dlist\ dxs{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
  13.183 +\isanewline
  13.184 +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
  13.185 +remove{\isadigit{1}}\ x\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline
  13.186 +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
  13.187 +\isanewline
  13.188 +remove\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Eq\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ Dlist\ a\ {\isacharminus}{\isachargreater}\ Dlist\ a{\isacharsemicolon}\isanewline
  13.189 +remove\ x\ dxs\ {\isacharequal}\ Dlist\ {\isacharparenleft}remove{\isadigit{1}}\ x\ {\isacharparenleft}list{\isacharunderscore}of{\isacharunderscore}dlist\ dxs{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
  13.190 +\isanewline
  13.191 +{\isacharbraceright}\isanewline
  13.192 +
  13.193 +  \end{typewriter}%
  13.194  \end{isamarkuptext}%
  13.195  \isamarkuptrue%
  13.196  %
    14.1 --- a/doc-src/Codegen/style.sty	Thu Sep 23 13:28:53 2010 +0200
    14.2 +++ b/doc-src/Codegen/style.sty	Thu Sep 23 15:46:17 2010 +0200
    14.3 @@ -26,9 +26,15 @@
    14.4  \renewcommand{\endisatagquote}{\end{quote}}
    14.5  \newcommand{\quotebreak}{\\[1.2ex]}
    14.6  
    14.7 +%% typewriter text
    14.8 +\newenvironment{typewriter}{\renewcommand{\isadigit}[1]{{##1}}%
    14.9 +\def\isacharunderscore{\_}%
   14.10 +\parindent0pt\fontsize{9pt}{0pt}%
   14.11 +\tt\setlength{\baselineskip}{8pt}\renewcommand{\baselinestretch}{1}}{}
   14.12 +
   14.13  \isakeeptag{quotett}
   14.14  \renewcommand{\isatagquotett}{\begin{quote}\isabellestyle{tt}\isastyle}
   14.15 -\renewcommand{\endisatagquotett}{\end{quote}\isabellestyle{it}\isastyle}
   14.16 +\renewcommand{\endisatagquotett}{\end{quote}}
   14.17  
   14.18  %% a trick
   14.19  \newcommand{\isasymSML}{SML}