diff -r bdb308737bfd -r 541366e3c1b3 doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Thu Oct 09 09:18:32 2008 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Thu Oct 09 18:16:07 2008 +0200
@@ -86,8 +86,8 @@
   but form a generic calculus, an instance of order-sorted
   algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}.
 
-  From a software engineering point of view, type classes
-  correspond to interfaces in object-oriented languages like Java;
+  From a software engeneering point of view, type classes
+  roughly correspond to interfaces in object-oriented languages like Java;
   so, it is naturally desirable that type classes do not only
   provide functions (class parameters) but also state specifications
   implementations must obey.  For example, the \isa{class\ eq}
@@ -111,7 +111,7 @@
   \begin{enumerate}
     \item specifying abstract parameters together with
        corresponding specifications,
-    \item instantating those abstract parameters by a particular
+    \item instantiating those abstract parameters by a particular
        type
     \item in connection with a ``less ad-hoc'' approach to overloading,
     \item with a direct link to the Isabelle module system
@@ -741,8 +741,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \ \ \isacommand{primrec}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\isanewline
-\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
 \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
@@ -806,9 +805,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \ \ \isacommand{fun}\isamarkupfalse%
-\isanewline
-\ \ \ \ \ \ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ list\ {\isasymRightarrow}\ {\isasymalpha}\ list{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{where}\isanewline
+\ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ list\ {\isasymRightarrow}\ {\isasymalpha}\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
 \ \ \ \ \ \ {\isachardoublequoteopen}replicate\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline
 \isanewline
@@ -822,15 +819,24 @@
 %
 \isatagproof
 \isacommand{proof}\isamarkupfalse%
+\ {\isacharminus}\isanewline
+\ \ \ \ \ \ \isacommand{interpret}\isamarkupfalse%
+\ monoid\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isacharat}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
 \isanewline
-\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
-\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
 \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ {\isacharparenleft}op\ {\isacharat}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
+\ n\isanewline
+\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ {\isacharparenleft}op\ {\isacharat}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
+\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}induct\ n{\isacharparenright}\ auto\isanewline
+\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
+\isanewline
 \ \ \ \ \isacommand{qed}\isamarkupfalse%
-%
+\ intro{\isacharunderscore}locales%
 \endisatagproof
 {\isafoldproof}%
 %
@@ -1006,21 +1012,171 @@
 \noindent This maps to Haskell as:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
-\ example\ \isakeyword{in}\ Haskell\ \isakeyword{module{\isacharunderscore}name}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}{\isachardoublequoteclose}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+%
 \begin{isamarkuptext}%
-\lsthaskell{Thy/code_examples/Classes.hs}
-
-  \noindent The whole code in SML with explicit dictionary passing:%
+\isaverbatim%
+\noindent%
+\verb|module Example where {|\newline%
+\newline%
+\newline%
+\verb|data Nat = Suc Nat |\verb,|,\verb| Zero_nat;|\newline%
+\newline%
+\verb|nat_aux :: Integer -> Nat -> Nat;|\newline%
+\verb|nat_aux i n = (if i <= 0 then n else nat_aux (i - 1) (Suc n));|\newline%
+\newline%
+\verb|nat :: Integer -> Nat;|\newline%
+\verb|nat i = nat_aux i Zero_nat;|\newline%
+\newline%
+\verb|class Semigroup a where {|\newline%
+\verb|  mult :: a -> a -> a;|\newline%
+\verb|};|\newline%
+\newline%
+\verb|class (Semigroup a) => Monoidl a where {|\newline%
+\verb|  neutral :: a;|\newline%
+\verb|};|\newline%
+\newline%
+\verb|class (Monoidl a) => Monoid a where {|\newline%
+\verb|};|\newline%
+\newline%
+\verb|class (Monoid a) => Group a where {|\newline%
+\verb|  inverse :: a -> a;|\newline%
+\verb|};|\newline%
+\newline%
+\verb|inverse_int :: Integer -> Integer;|\newline%
+\verb|inverse_int i = negate i;|\newline%
+\newline%
+\verb|neutral_int :: Integer;|\newline%
+\verb|neutral_int = 0;|\newline%
+\newline%
+\verb|mult_int :: Integer -> Integer -> Integer;|\newline%
+\verb|mult_int i j = i + j;|\newline%
+\newline%
+\verb|instance Semigroup Integer where {|\newline%
+\verb|  mult = mult_int;|\newline%
+\verb|};|\newline%
+\newline%
+\verb|instance Monoidl Integer where {|\newline%
+\verb|  neutral = neutral_int;|\newline%
+\verb|};|\newline%
+\newline%
+\verb|instance Monoid Integer where {|\newline%
+\verb|};|\newline%
+\newline%
+\verb|instance Group Integer where {|\newline%
+\verb|  inverse = inverse_int;|\newline%
+\verb|};|\newline%
+\newline%
+\verb|pow_nat :: forall a. (Monoid a) => Nat -> a -> a;|\newline%
+\verb|pow_nat Zero_nat x = neutral;|\newline%
+\verb|pow_nat (Suc n) x = mult x (pow_nat n x);|\newline%
+\newline%
+\verb|pow_int :: forall a. (Group a) => Integer -> a -> a;|\newline%
+\verb|pow_int k x =|\newline%
+\verb|  (if 0 <= k then pow_nat (nat k) x|\newline%
+\verb|    else inverse (pow_nat (nat (negate k)) x));|\newline%
+\newline%
+\verb|example :: Integer;|\newline%
+\verb|example = pow_int 10 (-2);|\newline%
+\newline%
+\verb|}|%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
-\ example\ \isakeyword{in}\ SML\ \isakeyword{module{\isacharunderscore}name}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}classes{\isachardot}ML{\isachardoublequoteclose}%
+%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
 \begin{isamarkuptext}%
-\lstsml{Thy/code_examples/classes.ML}%
+\noindent The whole code in SML with explicit dictionary passing:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+%
+\begin{isamarkuptext}%
+\isaverbatim%
+\noindent%
+\verb|structure Example = |\newline%
+\verb|struct|\newline%
+\newline%
+\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
+\newline%
+\verb|fun nat_aux i n =|\newline%
+\verb|  (if IntInf.<= (i, (0 : IntInf.int)) then n|\newline%
+\verb|    else nat_aux (IntInf.- (i, (1 : IntInf.int))) (Suc n));|\newline%
+\newline%
+\verb|fun nat i = nat_aux i Zero_nat;|\newline%
+\newline%
+\verb|type 'a semigroup = {mult : 'a -> 'a -> 'a};|\newline%
+\verb|fun mult (A_:'a semigroup) = #mult A_;|\newline%
+\newline%
+\verb|type 'a monoidl =|\newline%
+\verb|  {Classes__semigroup_monoidl : 'a semigroup, neutral : 'a};|\newline%
+\verb|fun semigroup_monoidl (A_:'a monoidl) = #Classes__semigroup_monoidl A_;|\newline%
+\verb|fun neutral (A_:'a monoidl) = #neutral A_;|\newline%
+\newline%
+\verb|type 'a monoid = {Classes__monoidl_monoid : 'a monoidl};|\newline%
+\verb|fun monoidl_monoid (A_:'a monoid) = #Classes__monoidl_monoid A_;|\newline%
+\newline%
+\verb|type 'a group = {Classes__monoid_group : 'a monoid, inverse : 'a -> 'a};|\newline%
+\verb|fun monoid_group (A_:'a group) = #Classes__monoid_group A_;|\newline%
+\verb|fun inverse (A_:'a group) = #inverse A_;|\newline%
+\newline%
+\verb|fun inverse_int i = IntInf.~ i;|\newline%
+\newline%
+\verb|val neutral_int : IntInf.int = (0 : IntInf.int);|\newline%
+\newline%
+\verb|fun mult_int i j = IntInf.+ (i, j);|\newline%
+\newline%
+\verb|val semigroup_int = {mult = mult_int} : IntInf.int semigroup;|\newline%
+\newline%
+\verb|val monoidl_int =|\newline%
+\verb|  {Classes__semigroup_monoidl = semigroup_int, neutral = neutral_int} :|\newline%
+\verb|  IntInf.int monoidl;|\newline%
+\newline%
+\verb|val monoid_int = {Classes__monoidl_monoid = monoidl_int} :|\newline%
+\verb|  IntInf.int monoid;|\newline%
+\newline%
+\verb|val group_int =|\newline%
+\verb|  {Classes__monoid_group = monoid_int, inverse = inverse_int} :|\newline%
+\verb|  IntInf.int group;|\newline%
+\newline%
+\verb|fun pow_nat A_ Zero_nat x = neutral (monoidl_monoid A_)|\newline%
+\verb|  |\verb,|,\verb| pow_nat A_ (Suc n) x =|\newline%
+\verb|    mult ((semigroup_monoidl o monoidl_monoid) A_) x (pow_nat A_ n x);|\newline%
+\newline%
+\verb|fun pow_int A_ k x =|\newline%
+\verb|  (if IntInf.<= ((0 : IntInf.int), k)|\newline%
+\verb|    then pow_nat (monoid_group A_) (nat k) x|\newline%
+\verb|    else inverse A_ (pow_nat (monoid_group A_) (nat (IntInf.~ k)) x));|\newline%
+\newline%
+\verb|val example : IntInf.int =|\newline%
+\verb|  pow_int group_int (10 : IntInf.int) (~2 : IntInf.int);|\newline%
+\newline%
+\verb|end; (*struct Example*)|%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
 \isadelimtheory
 %
 \endisadelimtheory