doc-src/TutorialI/Types/types.tex
changeset 14400 6069098854b9
parent 12568 a46009d88687
child 25257 8faf184ba5b1
     1.1 --- a/doc-src/TutorialI/Types/types.tex	Thu Feb 19 16:44:21 2004 +0100
     1.2 +++ b/doc-src/TutorialI/Types/types.tex	Thu Feb 19 17:57:54 2004 +0100
     1.3 @@ -6,37 +6,29 @@
     1.4  (\isacommand{datatype}). This chapter will introduce more
     1.5  advanced material:
     1.6  \begin{itemize}
     1.7 -\item More about basic types: numbers ({\S}\ref{sec:numbers}), pairs
     1.8 -  ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}), and how to
     1.9 -  reason about them.
    1.10 +\item Pairs ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}),
    1.11 and how to reason about them.
    1.12  \item Type classes: how to specify and reason about axiomatic collections of
    1.13 -  types ({\S}\ref{sec:axclass}).
    1.14 -\item Introducing your own types: how to introduce new types that
    1.15 +  types ({\S}\ref{sec:axclass}). This section leads on to a discussion of
    1.16 +  Isabelle's numeric types ({\S}\ref{sec:numbers}).  
    1.17 +\item Introducing your own types: how to define types that
    1.18    cannot be constructed with any of the basic methods
    1.19    ({\S}\ref{sec:adv-typedef}).
    1.20  \end{itemize}
    1.21  
    1.22 -The material in this section goes beyond the needs of most novices.  Serious
    1.23 -users should at least skim the sections on basic types and on type classes.
    1.24 -The latter material is fairly advanced; read the beginning to understand what
    1.25 -it is 
    1.26 -about, but consult the rest only when necessary.
    1.27 -
    1.28 -\input{Types/numerics}
    1.29 +The material in this section goes beyond the needs of most novices.
    1.30 Serious users should at least skim the sections as far as type classes.
    1.31 That material is fairly advanced; read the beginning to understand what it
    1.32 is about, but consult the rest only when necessary.
    1.33  
    1.34  \index{pairs and tuples|(}
    1.35 -\input{Types/document/Pairs}
    1.36 +\input{Types/document/Pairs}    %%%Section "Pairs and Tuples"
    1.37  \index{pairs and tuples|)}
    1.38  
    1.39 -\input{Types/document/Records}
    1.40 +\input{Types/document/Records}  %%%Section "Records"
    1.41  
    1.42  
    1.43 -\section{Axiomatic Type Classes}
    1.44 +\section{Axiomatic Type Classes} %%%Section
    1.45  \label{sec:axclass}
    1.46  \index{axiomatic type classes|(}
    1.47  \index{*axclass|(}
    1.48  
    1.49 -
    1.50  The programming language Haskell has popularized the notion of type classes.
    1.51  In its simplest form, a type class is a set of types with a common interface:
    1.52  all types in that class must provide the functions in the interface.
    1.53 @@ -67,5 +59,6 @@
    1.54  \index{axiomatic type classes|)}
    1.55  \index{*axclass|)}
    1.56  
    1.57 +\input{Types/numerics}             %%%Section "Numbers"
    1.58  
    1.59 -\input{Types/document/Typedefs}
    1.60 +\input{Types/document/Typedefs}    %%%Section "Introducing New Types"