updated

--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Tue Jul 24 15:20:53 2007 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Tue Jul 24 15:21:54 2007 +0200
@@ -3,7 +3,7 @@
 
 (*<*)
 theory Classes
-imports Main
+imports Main Pretty_Int
 begin
 
 ML {*
@@ -106,7 +106,7 @@
 
   Indeed, type classes not only allow for simple overloading
   but form a generic calculus, an instance of order-sorted
-  algebra \cite{Nipkow-Prehofer:1993,Nipkow:1993,Wenzel:1997}.
+  algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}.
 
   From a software enigineering point of view, type classes
   correspond to interfaces in object-oriented languages like Java;
@@ -136,7 +136,8 @@
     \item instantating those abstract operations 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 (aka locales).
+    \item with a direct link to the Isabelle module system
+      (aka locales \cite{kammueller-locales}).
   \end{enumerate}
 
   \noindent Isar type classes also directly support code generation
@@ -145,12 +146,12 @@
   This tutorial demonstrates common elements of structured specifications
   and abstract reasoning with type classes by the algebraic hierarchy of
   semigroups, monoids and groups.  Our background theory is that of
-  Isabelle/HOL \cite{Nipkow-et-al:2002:tutorial}, for which some
+  Isabelle/HOL \cite{isa-tutorial}, for which some
   familiarity is assumed.
 
   Here we merely present the look-and-feel for end users.
   Internally, those are mapped to more primitive Isabelle concepts.
-  See \cite{haftmann_wenzel2006classes} for more detail.
+  See \cite{Haftmann-Wenzel:2006:classes} for more detail.
 *}
 
 section {* A simple algebra example \label{sec:example} *}
@@ -403,12 +404,33 @@
 *}
 
 
-(*subsection {* Derived definitions *}
+subsection {* Derived definitions *}
+
+text {*
+  Isabelle locales support a concept of local definitions
+  in locales:
+*}
+
+    fun (in monoid)
+      pow_nat :: "nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
+      "pow_nat 0 x = \<^loc>\<one>"
+      | "pow_nat (Suc n) x = x \<^loc>\<otimes> pow_nat n x"
 
 text {*
-*}*)
+  \noindent If the locale @{text group} is also a class, this local
+  definition is propagated onto a global definition of
+  @{term [source] "pow_nat \<Colon> nat \<Rightarrow> \<alpha>\<Colon>monoid \<Rightarrow> \<alpha>\<Colon>monoid"}
+  with corresponding theorems
+
+  @{thm pow_nat.simps [no_vars]}.
 
-(* subsection {* Additional subclass relations *}
+  \noindent As you can see from this example, for local
+  definitions you may use any specification tool
+  which works together with locales (e.g. \cite{krauss2006}).
+*}
+
+
+(*subsection {* Additional subclass relations *}
 
 text {*
   Any @{text "group"} is also a @{text "monoid"};  this
@@ -416,13 +438,36 @@
   together with a proof of the logical difference:
 *}
 
-    instance group < monoid
-    proof -
+    instance advanced group < monoid
+    proof unfold_locales
       fix x
       from invl have "x\<^loc>\<div> \<^loc>\<otimes> x = \<^loc>\<one>" by simp
       with assoc [symmetric] neutl invl have "x\<^loc>\<div> \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<one>) = x\<^loc>\<div> \<^loc>\<otimes> x" by simp
       with left_cancel show "x \<^loc>\<otimes> \<^loc>\<one> = x" by simp
-    qed *)
+    qed
+
+text {*
+  The logical proof is carried out on the locale level
+  and thus conveniently is opened using the @{text unfold_locales}
+  method which only leaves the logical differences still
+  open to proof to the user.  After the proof it is propagated
+  to the type system, making @{text group} an instance of
+  @{text monoid}.  For illustration, a derived definition
+  in @{text group} which uses @{text of_nat}:
+*}
+
+    definition (in group)
+      pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
+      "pow_int k x = (if k >= 0
+        then pow_nat (nat k) x
+        else (pow_nat (nat (- k)) x)\<^loc>\<div>)"
+
+text {*
+  yields the global definition of
+  @{term [source] "pow_int \<Colon> int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"}
+  with the corresponding theorem @{thm pow_int_def [no_vars]}.
+*} *)
+
 
 section {* Further issues *}
 
@@ -437,11 +482,11 @@
   takes this into account.  Concerning target languages
   lacking type classes (e.g.~SML), type classes
   are implemented by explicit dictionary construction.
-  As example, the natural power function on groups:
+  For example, lets go back to the power function:
 *}
 
     fun
-      pow_nat :: "nat \<Rightarrow> \<alpha>\<Colon>monoidl \<Rightarrow> \<alpha>\<Colon>monoidl" where
+      pow_nat :: "nat \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group" where
       "pow_nat 0 x = \<one>"
       | "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
 
@@ -459,19 +504,17 @@
   \noindent This maps to Haskell as:
 *}
 
-code_gen example in Haskell file "code_examples/"
+code_gen example in Haskell to Classes file "code_examples/"
   (* NOTE: you may use Haskell only once in this document, otherwise
   you have to work in distinct subdirectories *)
 
 text {*
   \lsthaskell{Thy/code_examples/Classes.hs}
 
-  \noindent (we have left out all other modules).
-
   \noindent The whole code in SML with explicit dictionary passing:
 *}
 
-code_gen example (*<*)in SML(*>*)in SML file "code_examples/classes.ML"
+code_gen example (*<*)in SML to Classes(*>*)in SML to Classes file "code_examples/classes.ML"
 
 text {*
   \lstsml{Thy/code_examples/classes.ML}

--- a/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs	Tue Jul 24 15:20:53 2007 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs	Tue Jul 24 15:21:54 2007 +0200
@@ -1,61 +1,59 @@
 module Classes where {
 
-import qualified Integer;
-import qualified Nat;
+
+data Nat = Zero_nat | Suc Nat;
+
+data Bit = B0 | B1;
+
+nat_aux :: Integer -> Nat -> Nat;
+nat_aux i n = (if i <= 0 then n else nat_aux (i - 1) (Suc n));
+
+nat :: Integer -> Nat;
+nat i = nat_aux i Zero_nat;
 
 class Semigroup a where {
   mult :: a -> a -> a;
 };
 
-class (Classes.Semigroup a) => Monoidl a where {
+class (Semigroup a) => Monoidl a where {
   neutral :: a;
 };
 
-class (Classes.Monoidl a) => Group a where {
+class (Monoidl a) => Group a where {
   inverse :: a -> a;
 };
 
-inverse_int :: Integer.Inta -> Integer.Inta;
-inverse_int i = Integer.uminus_int i;
+inverse_int :: Integer -> Integer;
+inverse_int i = negate i;
 
-neutral_int :: Integer.Inta;
-neutral_int = Integer.Number_of_int Integer.Pls;
+neutral_int :: Integer;
+neutral_int = 0;
 
-mult_int :: Integer.Inta -> Integer.Inta -> Integer.Inta;
-mult_int i j = Integer.plus_int i j;
+mult_int :: Integer -> Integer -> Integer;
+mult_int i j = i + j;
 
-instance Classes.Semigroup Integer.Inta where {
-  mult = Classes.mult_int;
+instance Semigroup Integer where {
+  mult = mult_int;
 };
 
-instance Classes.Monoidl Integer.Inta where {
-  neutral = Classes.neutral_int;
-};
-
-instance Classes.Group Integer.Inta where {
-  inverse = Classes.inverse_int;
+instance Monoidl Integer where {
+  neutral = neutral_int;
 };
 
-pow_nat :: (Classes.Monoidl b) => Nat.Nat -> b -> b;
-pow_nat (Nat.Suc n) x = Classes.mult x (Classes.pow_nat n x);
-pow_nat Nat.Zero_nat x = Classes.neutral;
+instance Group Integer where {
+  inverse = inverse_int;
+};
 
-pow_int :: (Classes.Group a) => Integer.Inta -> a -> a;
-pow_int k x =
-  (if Integer.less_eq_int (Integer.Number_of_int Integer.Pls) k
-    then Classes.pow_nat (Integer.nat k) x
-    else Classes.inverse
-           (Classes.pow_nat (Integer.nat (Integer.uminus_int k)) x));
+pow_nat :: (Group b) => Nat -> b -> b;
+pow_nat (Suc n) x = mult x (pow_nat n x);
+pow_nat Zero_nat x = neutral;
 
-example :: Integer.Inta;
-example =
-  Classes.pow_int
-    (Integer.Number_of_int
-      (Integer.Bit
-        (Integer.Bit
-          (Integer.Bit (Integer.Bit Integer.Pls Integer.B1) Integer.B0)
-          Integer.B1)
-        Integer.B0))
-    (Integer.Number_of_int (Integer.Bit Integer.Min Integer.B0));
+pow_int :: (Group a) => Integer -> a -> a;
+pow_int k x =
+  (if 0 <= k then pow_nat (nat k) x
+    else inverse (pow_nat (nat (negate k)) x));
+
+example :: Integer;
+example = pow_int 10 (-2);
 
 }

--- a/doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML	Tue Jul 24 15:20:53 2007 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML	Tue Jul 24 15:21:54 2007 +0200
@@ -1,141 +1,53 @@
-structure ROOT = 
-struct
-
-structure Nat = 
+structure Classes = 
 struct
 
 datatype nat = Zero_nat | Suc of nat;
 
-end; (*struct Nat*)
-
-structure Integer = 
-struct
-
 datatype bit = B0 | B1;
 
-datatype int = Pls | Min | Bit of int * bit | Number_of_int of int;
-
-fun pred (Bit (k, B0)) = Bit (pred k, B1)
-  | pred (Bit (k, B1)) = Bit (k, B0)
-  | pred Min = Bit (Min, B0)
-  | pred Pls = Min;
-
-fun uminus_int (Number_of_int w) = Number_of_int (uminus_int w)
-  | uminus_int (Bit (k, B0)) = Bit (uminus_int k, B0)
-  | uminus_int (Bit (k, B1)) = Bit (pred (uminus_int k), B1)
-  | uminus_int Min = Bit (Pls, B1)
-  | uminus_int Pls = Pls;
-
-fun succ (Bit (k, B0)) = Bit (k, B1)
-  | succ (Bit (k, B1)) = Bit (succ k, B0)
-  | succ Min = Pls
-  | succ Pls = Bit (Pls, B1);
-
-fun plus_int (Number_of_int v) (Number_of_int w) =
-  Number_of_int (plus_int v w)
-  | plus_int k Min = pred k
-  | plus_int k Pls = k
-  | plus_int (Bit (k, B1)) (Bit (l, B1)) = Bit (plus_int k (succ l), B0)
-  | plus_int (Bit (k, B1)) (Bit (l, B0)) = Bit (plus_int k l, B1)
-  | plus_int (Bit (k, B0)) (Bit (l, b)) = Bit (plus_int k l, b)
-  | plus_int Min k = pred k
-  | plus_int Pls k = k;
-
-fun minus_int (Number_of_int v) (Number_of_int w) =
-  Number_of_int (plus_int v (uminus_int w))
-  | minus_int z w = plus_int z (uminus_int w);
+fun nat_aux i n =
+  (if IntInf.<= (i, (0 : IntInf.int)) then n
+    else nat_aux (IntInf.- (i, (1 : IntInf.int))) (Suc n));
 
-fun less_eq_int (Number_of_int k) (Number_of_int l) = less_eq_int k l
-  | less_eq_int (Bit (k1, B1)) (Bit (k2, B0)) = less_int k1 k2
-  | less_eq_int (Bit (k1, v)) (Bit (k2, B1)) = less_eq_int k1 k2
-  | less_eq_int (Bit (k1, B0)) (Bit (k2, v)) = less_eq_int k1 k2
-  | less_eq_int (Bit (k, v)) Min = less_eq_int k Min
-  | less_eq_int (Bit (k, B1)) Pls = less_int k Pls
-  | less_eq_int (Bit (k, B0)) Pls = less_eq_int k Pls
-  | less_eq_int Min (Bit (k, B1)) = less_eq_int Min k
-  | less_eq_int Min (Bit (k, B0)) = less_int Min k
-  | less_eq_int Min Min = true
-  | less_eq_int Min Pls = true
-  | less_eq_int Pls (Bit (k, v)) = less_eq_int Pls k
-  | less_eq_int Pls Min = false
-  | less_eq_int Pls Pls = true
-and less_int (Number_of_int k) (Number_of_int l) = less_int k l
-  | less_int (Bit (k1, B0)) (Bit (k2, B1)) = less_eq_int k1 k2
-  | less_int (Bit (k1, B1)) (Bit (k2, v)) = less_int k1 k2
-  | less_int (Bit (k1, v)) (Bit (k2, B0)) = less_int k1 k2
-  | less_int (Bit (k, B1)) Min = less_int k Min
-  | less_int (Bit (k, B0)) Min = less_eq_int k Min
-  | less_int (Bit (k, v)) Pls = less_int k Pls
-  | less_int Min (Bit (k, v)) = less_int Min k
-  | less_int Min Min = false
-  | less_int Min Pls = true
-  | less_int Pls (Bit (k, B1)) = less_eq_int Pls k
-  | less_int Pls (Bit (k, B0)) = less_int Pls k
-  | less_int Pls Min = false
-  | less_int Pls Pls = false;
-
-fun nat_aux n i =
-  (if less_eq_int i (Number_of_int Pls) then n
-    else nat_aux (Nat.Suc n)
-           (minus_int i (Number_of_int (Bit (Pls, B1)))));
-
-fun nat i = nat_aux Nat.Zero_nat i;
-
-end; (*struct Integer*)
-
-structure Classes = 
-struct
+fun nat i = nat_aux i Zero_nat;
 
 type 'a semigroup = {mult : 'a -> 'a -> 'a};
 fun mult (A_:'a semigroup) = #mult A_;
 
 type 'a monoidl =
-  {Classes__monoidl_semigroup : 'a semigroup, neutral : 'a};
-fun monoidl_semigroup (A_:'a monoidl) = #Classes__monoidl_semigroup A_;
+  {Classes__semigroup_monoidl : 'a semigroup, neutral : 'a};
+fun semigroup_monoidl (A_:'a monoidl) = #Classes__semigroup_monoidl A_;
 fun neutral (A_:'a monoidl) = #neutral A_;
 
-type 'a group = {Classes__group_monoidl : 'a monoidl, inverse : 'a -> 'a};
-fun group_monoidl (A_:'a group) = #Classes__group_monoidl A_;
+type 'a group = {Classes__monoidl_group : 'a monoidl, inverse : 'a -> 'a};
+fun monoidl_group (A_:'a group) = #Classes__monoidl_group A_;
 fun inverse (A_:'a group) = #inverse A_;
 
-fun inverse_int i = Integer.uminus_int i;
+fun inverse_int i = IntInf.~ i;
 
-val neutral_int : Integer.int = Integer.Number_of_int Integer.Pls;
+val neutral_int : IntInf.int = (0 : IntInf.int);
 
-fun mult_int i j = Integer.plus_int i j;
+fun mult_int i j = IntInf.+ (i, j);
 
-val semigroup_int = {mult = mult_int} : Integer.int semigroup;
+val semigroup_int = {mult = mult_int} : IntInf.int semigroup;
 
 val monoidl_int =
-  {Classes__monoidl_semigroup = semigroup_int, neutral = neutral_int} :
-  Integer.int monoidl;
+  {Classes__semigroup_monoidl = semigroup_int, neutral = neutral_int} :
+  IntInf.int monoidl;
 
 val group_int =
-  {Classes__group_monoidl = monoidl_int, inverse = inverse_int} :
-  Integer.int group;
+  {Classes__monoidl_group = monoidl_int, inverse = inverse_int} :
+  IntInf.int group;
 
-fun pow_nat B_ (Nat.Suc n) x =
-  mult (monoidl_semigroup B_) x (pow_nat B_ n x)
-  | pow_nat B_ Nat.Zero_nat x = neutral B_;
+fun pow_nat B_ (Suc n) x =
+  mult ((semigroup_monoidl o monoidl_group) B_) x (pow_nat B_ n x)
+  | pow_nat B_ Zero_nat x = neutral (monoidl_group B_);
 
 fun pow_int A_ k x =
-  (if Integer.less_eq_int (Integer.Number_of_int Integer.Pls) k
-    then pow_nat (group_monoidl A_) (Integer.nat k) x
-    else inverse A_
-           (pow_nat (group_monoidl A_)
-             (Integer.nat (Integer.uminus_int k)) x));
+  (if IntInf.<= ((0 : IntInf.int), k) then pow_nat A_ (nat k) x
+    else inverse A_ (pow_nat A_ (nat (IntInf.~ k)) x));
 
-val example : Integer.int =
-  pow_int group_int
-    (Integer.Number_of_int
-      (Integer.Bit
-        (Integer.Bit
-           (Integer.Bit
-              (Integer.Bit (Integer.Pls, Integer.B1), Integer.B0),
-             Integer.B1),
-          Integer.B0)))
-    (Integer.Number_of_int (Integer.Bit (Integer.Min, Integer.B0)));
+val example : IntInf.int =
+  pow_int group_int (10 : IntInf.int) (~2 : IntInf.int);
 
 end; (*struct Classes*)
-
-end; (*struct ROOT*)

--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Tue Jul 24 15:20:53 2007 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Tue Jul 24 15:21:54 2007 +0200
@@ -85,7 +85,7 @@
 
   Indeed, type classes not only allow for simple overloading
   but form a generic calculus, an instance of order-sorted
-  algebra \cite{Nipkow-Prehofer:1993,Nipkow:1993,Wenzel:1997}.
+  algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}.
 
   From a software enigineering point of view, type classes
   correspond to interfaces in object-oriented languages like Java;
@@ -115,7 +115,8 @@
     \item instantating those abstract operations 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 (aka locales).
+    \item with a direct link to the Isabelle module system
+      (aka locales \cite{kammueller-locales}).
   \end{enumerate}
 
   \noindent Isar type classes also directly support code generation
@@ -124,12 +125,12 @@
   This tutorial demonstrates common elements of structured specifications
   and abstract reasoning with type classes by the algebraic hierarchy of
   semigroups, monoids and groups.  Our background theory is that of
-  Isabelle/HOL \cite{Nipkow-et-al:2002:tutorial}, for which some
+  Isabelle/HOL \cite{isa-tutorial}, for which some
   familiarity is assumed.
 
   Here we merely present the look-and-feel for end users.
   Internally, those are mapped to more primitive Isabelle concepts.
-  See \cite{haftmann_wenzel2006classes} for more detail.%
+  See \cite{Haftmann-Wenzel:2006:classes} for more detail.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -662,6 +663,35 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsubsection{Derived definitions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isabelle locales support a concept of local definitions
+  in locales:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ \ \ \isacommand{fun}\isamarkupfalse%
+\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\isanewline
+\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ \isactrlloc {\isasymone}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\noindent If the locale \isa{group} is also a class, this local
+  definition is propagated onto a global definition of
+  \isa{{\isachardoublequote}pow{\isacharunderscore}nat\ {\isasymColon}\ nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid{\isachardoublequote}}
+  with corresponding theorems
+
+  \isa{pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}\isasep\isanewline%
+pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x}.
+
+  \noindent As you can see from this example, for local
+  definitions you may use any specification tool
+  which works together with locales (e.g. \cite{krauss2006}).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsection{Further issues%
 }
 \isamarkuptrue%
@@ -679,12 +709,12 @@
   takes this into account.  Concerning target languages
   lacking type classes (e.g.~SML), type classes
   are implemented by explicit dictionary construction.
-  As example, the natural power function on groups:%
+  For example, lets go back to the power function:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \ \ \isacommand{fun}\isamarkupfalse%
 \isanewline
-\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoidl\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoidl{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\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}\isanewline
 \isanewline
@@ -704,17 +734,15 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ example\ \isakeyword{in}\ Haskell\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}{\isachardoublequoteclose}%
+\ example\ \isakeyword{in}\ Haskell\ \isakeyword{to}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \lsthaskell{Thy/code_examples/Classes.hs}
 
-  \noindent (we have left out all other modules).
-
   \noindent The whole code in SML with explicit dictionary passing:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ example\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}classes{\isachardot}ML{\isachardoublequoteclose}%
+\ example\ \isakeyword{in}\ SML\ \isakeyword{to}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}classes{\isachardot}ML{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \lstsml{Thy/code_examples/classes.ML}%
 \end{isamarkuptext}%

--- a/doc-src/IsarAdvanced/Classes/classes.bib	Tue Jul 24 15:20:53 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,211 +0,0 @@
-
-@InProceedings{Ballarin:2004,
-  author = 	 {Clemens Ballarin},
-  title = 	 {Locales and Locale Expressions in {Isabelle/Isar}},
-  booktitle =	 {Types for Proofs and Programs (TYPES 2003)},
-  year =	 2004,
-  editor =	 {Stefano Berardi and others},
-  series =	 {LNCS 3085}
-}
-
-@InProceedings{Ballarin:2006,
-  author = 	 {Clemens Ballarin},
-  title = 	 {Interpretation of Locales in {Isabelle}: Theories and Proof Contexts},
-  booktitle =	 {Mathematical Knowledge Management (MKM 2006)},
-  year =	 2006,
-  editor =	 {J.M. Borwein and W.M. Farmer},
-  series =	 {LNAI 4108}
-}
-
-@InProceedings{Berghofer-Nipkow:2000,
-  author =       {Stefan Berghofer and Tobias Nipkow},
-  title =        {Proof terms for simply typed higher order logic},
-  booktitle     = {Theorem Proving in Higher Order Logics ({TPHOLs} 2000)},
-  editor        = {J. Harrison and M. Aagaard},
-  series        = {LNCS 1869},
-  year          = 2000
-}
-
-@Manual{Coq-Manual:2006,
-  title =        {The {Coq} Proof Assistant Reference Manual, version 8},
-  author =       {B. Barras and others},
-  organization = {INRIA},
-  year =         2006
-}
-
-@Article{Courant:2006,
-  author = 	 {Judica{\"e}l Courant},
-  title = 	 {{$\mathcal{MC}_2$: A Module Calculus for Pure Type Systems}},
-  journal = 	 {The Journal of Functional Programming},
-  year = 	 2006,
-  note =	 {To appear},
-  abstract = {Several proof-assistants rely on the very formal basis
-    of Pure Type Systems (PTS) as their foundations.  We are concerned
-    with the issues involved in the development of large proofs in
-    these provers such as namespace management, development of
-    reusable proof libraries and separate verification. Although
-    implementations offer many features to address them, few
-    theoretical foundations have been laid for them up to now. This is
-    a problem as features dealing with modularity may have harmful,
-    unsuspected effects on the reliability or usability of an
-    implementation.
-    
-    In this paper, we propose an extension of Pure Type Systems with a
-    module system, MC2, adapted from SML-like module systems for
-    programming languages.  This system gives a theoretical framework
-    addressing the issues mentioned above in a quite uniform way.  It
-    is intended to be a theoretical foundation for the module systems
-    of proof-assistants such as Coq or Agda.  We show how reliability
-    and usability can be formalized as metatheoretical properties and
-    prove they hold for MC2.}
-}
-
-@PhdThesis{Jacek:2004,
-  author = 	 {Jacek Chrz\c{a}szcz},
-  title = 	 {Modules in type theory with generative definitions},
-  school = 	 {Universit{\'e} Paris-Sud},
-  year = 	 {2004},
-}
-
-@InProceedings{Kamm-et-al:1999,
-  author =       {Florian Kamm{\"u}ller and Markus Wenzel and
-                  Lawrence C. Paulson},
-  title =        {Locales: A Sectioning Concept for {Isabelle}},
-  booktitle     = {Theorem Proving in Higher Order Logics ({TPHOLs} '99)},
-  editor        = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and
-                  Paulin, C. and Thery, L.},
-  series        = {LNCS 1690},
-  year          = 1999
-}
-
-@InProceedings{Nipkow-Prehofer:1993,
-  author =       {T. Nipkow and C. Prehofer},
-  title =        {Type checking type classes},
-  booktitle =    {ACM Symp.\ Principles of Programming Languages},
-  year =         1993
-}
-
-@Book{Nipkow-et-al:2002:tutorial,
-  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
-  title		= {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
-  series	= {LNCS 2283},
-  year		= 2002
-}
-
-@InCollection{Nipkow:1993,
-  author =       {T. Nipkow},
-  title =        {Order-Sorted Polymorphism in {Isabelle}},
-  booktitle =    {Logical Environments},
-  publisher =    {Cambridge University Press},
-  year =         1993,
-  editor =       {G. Huet and G. Plotkin}
-}
-
-@InProceedings{Nipkow:2002,
-  author = 	 {Tobias Nipkow},
-  title = 	 {Structured Proofs in {Isar/HOL}},
-  booktitle = 	 {Types for Proofs and Programs (TYPES 2002)},
-  year =	 2003,
-  editor =	 {H. Geuvers and F. Wiedijk},
-  series =	 {LNCS 2646}
-}
-
-@InCollection{Paulson:1990,
-  author =       {L. C. Paulson},
-  title =        {Isabelle: the next 700 theorem provers},
-  booktitle =    {Logic and Computer Science},
-  publisher =    {Academic Press},
-  year =         1990,
-  editor =       {P. Odifreddi}
-}
-
-@BOOK{Pierce:TypeSystems,
-  AUTHOR = {B.C. Pierce},
-  TITLE = {Types and Programming Languages},
-  PUBLISHER = {MIT Press},
-  YEAR = 2002,
-  PLCLUB = {Yes},
-  BCP = {Yes},
-  KEYS = {books},
-  HOMEPAGE = {http://www.cis.upenn.edu/~bcpierce/tapl},
-  ERRATA = {http://www.cis.upenn.edu/~bcpierce/tapl/errata.txt}
-}
-
-@Book{Schmidt-Schauss:1989,
-  author	= {Manfred Schmidt-Schau{\ss}},
-  title		= {Computational Aspects of an Order-Sorted Logic with Term Declarations},
-  series	= {LNAI 395},
-  year		= 1989
-}
-
-@InProceedings{Wenzel:1997,
-  author =       {M. Wenzel},
-  title =        {Type Classes and Overloading in Higher-Order Logic},
-  booktitle =    {Theorem Proving in Higher Order Logics ({TPHOLs} '97)},
-  editor =       {Elsa L. Gunter and Amy Felty},
-  series =       {LNCS 1275},
-  year =         1997}
-
-@article{hall96type,
-  author = "Cordelia Hall and Kevin Hammond and Peyton Jones, S. and Philip Wadler",
-  title = "Type Classes in {Haskell}",
-  journal = "ACM Transactions on Programming Languages and Systems",
-  volume = "18",
-  number = "2",
-  publisher = "ACM Press",
-  year = "1996"
-}
-
-@inproceedings{hindleymilner,
-  author = {L. Damas and H. Milner},
-  title = {Principal type schemes for functional programs},
-  booktitle = {ACM Symp. Principles of Programming Languages},
-  year = 1982
-}
-
-@manual{isabelle-axclass,
-  author	= {Markus Wenzel},
-  title		= {Using Axiomatic Type Classes in {I}sabelle},
-  institution	= {TU Munich},
-  year          = 2005,
-  note          = {\url{http://isabelle.in.tum.de/doc/axclass.pdf}}}
-
-@InProceedings{krauss:2006:functions,
-  author = 	 {A. Krauss},
-  title = 	 {Partial Recursive Functions in Higher-Order Logic},
-  booktitle = 	 {Int. Joint Conference on Automated Reasoning (IJCAR 2006)},
-  year =	 2006,
-  editor =	 {Ulrich Furbach and Natarajan Shankar},
-  series =	 {LNCS}
-}
-
-@inproceedings{peterson93implementing,
-  author = "J. Peterson and Peyton Jones, S.",
-  title = "Implementing Type Classes",
-  booktitle = "{SIGPLAN} Conference on Programming Language Design and Implementation",
-  year = 1993
-}
-
-@inproceedings{wadler89how,
-  author = {P. Wadler and S. Blott},
-  title = {How to make ad-hoc polymorphism less ad-hoc},
-  booktitle = {ACM Symp.\ Principles of Programming Languages},
-  year = 1989
-}
-
-@misc{jones97type,
-  author = "S. Jones and M. Jones and E. Meijer",
-  title = "Type classes: an exploration of the design space",
-  text = "Simon Peyton Jones, Mark Jones, and Erik Meijer. Type classes: an exploration
-    of the design space. In Haskell Workshop, June 1997.",
-  year = "1997",
-  url = "citeseer.ist.psu.edu/peytonjones97type.html"
-}
-
-@article{haftmann_wenzel2006classes,
-  author = "Florian Haftmann and Makarius Wenzel",
-  title =  "Constructive Type Classes in Isabelle",
-  year =   2006,
-  note =   {To appear}
-}
-

--- a/doc-src/IsarAdvanced/Classes/classes.tex	Tue Jul 24 15:20:53 2007 +0200
+++ b/doc-src/IsarAdvanced/Classes/classes.tex	Tue Jul 24 15:21:54 2007 +0200
@@ -79,7 +79,7 @@
 \begingroup
 %\tocentry{\bibname}
 \bibliographystyle{plain} \small\raggedright\frenchspacing
-\bibliography{../../manual,classes}
+\bibliography{../../manual}
 \endgroup
 
 \end{document}

--- a/doc-src/manual.bib	Tue Jul 24 15:20:53 2007 +0200
+++ b/doc-src/manual.bib	Tue Jul 24 15:21:54 2007 +0200
@@ -441,6 +441,13 @@
 
 %H
 
+@InProceedings{Haftmann-Wenzel:2006:classes,
+  author        = {Florian Haftmann and Makarius Wenzel},
+  title         = {Constructive Type Classes in {Isabelle}},
+  year          =   2006,
+  note          =   {To appear}
+}
+
 @manual{isabelle-classes,
   author	= {Florian Haftmann},
   title		= {Haskell-style type classes with {Isabelle}/{Isar}},
@@ -803,6 +810,13 @@
   year		= 1995,
   pages		= {201-224}}
 
+@InProceedings{Nipkow-Prehofer:1993,
+  author =       {T. Nipkow and C. Prehofer},
+  title =        {Type checking type classes},
+  booktitle =    {ACM Symp.\ Principles of Programming Languages},
+  year =         1993
+}
+
 @Book{isa-tutorial,
   author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
   title		= {Isabelle/HOL: A Proof Assistant for Higher-Order Logic},
@@ -1231,6 +1245,13 @@
 
 %W
 
+@inproceedings{wadler89how,
+  author        = {P. Wadler and S. Blott},
+  title         = {How to make ad-hoc polymorphism less ad-hoc},
+  booktitle     = {ACM Symp.\ Principles of Programming Languages},
+  year          = 1989
+}
+
 @Misc{x-symbol,
   author =	 {Christoph Wedler},
   title =	 {Emacs package ``{X-Symbol}''},
@@ -1531,6 +1552,6 @@
   year          = 2006}
 
 @unpublished{classes_modules,
-  title         = {ML Modules and Haskell Type Classes: A Constructive Comparison},
+  title         = {{ML} Modules and {Haskell} Type Classes: A Constructive Comparison},
   author        = {Stefan Wehr et. al.}
 }