1.1 --- a/doc-src/TutorialI/Types/types.tex	Tue May 01 17:16:32 2001 +0200
     1.2 +++ b/doc-src/TutorialI/Types/types.tex	Tue May 01 22:26:55 2001 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4  \label{ch:more-types}
     1.5  
     1.6  So far we have learned about a few basic types (for example \isa{bool} and
     1.7 -\isa{nat}), type abbreviations (\isacommand{types}) and recursive datatpes
     1.8 +\isa{nat}), type abbreviations (\isacommand{types}) and recursive datatypes
     1.9  (\isacommand{datatype}). This chapter will introduce more
    1.10  advanced material:
    1.11  \begin{itemize}
    1.12 @@ -33,13 +33,15 @@
    1.13  \section{Records}
    1.14  \label{sec:records}
    1.15  
    1.16 -\section{Axiomatic type classes}
    1.17 +\section{Axiomatic Type Classes}
    1.18  \label{sec:axclass}
    1.19  \index{axiomatic type class|(}
    1.20  \index{*axclass|(}
    1.21  
    1.22  
    1.23  The programming language Haskell has popularized the notion of type classes.
    1.24 +In its simplest form, a type class is a set of types with a common interface:
    1.25 +all types in that class must provide the functions in the interface.
    1.26  Isabelle offers the related concept of an \textbf{axiomatic type class}.
    1.27  Roughly speaking, an axiomatic type class is a type class with axioms, i.e.\ 
    1.28  an axiomatic specification of a class of types. Thus we can talk about a type