--- a/doc-src/TutorialI/document/types0.tex Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-\chapter{More about Types}
-\label{ch:more-types}
-
-So far we have learned about a few basic types (for example \isa{bool} and
-\isa{nat}), type abbreviations (\isacommand{types}) and recursive datatypes
-(\isacommand{datatype}). This chapter will introduce more
-advanced material:
-\begin{itemize}
-\item Pairs ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}),
-and how to reason about them.
-\item Type classes: how to specify and reason about axiomatic collections of
- types ({\S}\ref{sec:axclass}). This section leads on to a discussion of
- Isabelle's numeric types ({\S}\ref{sec:numbers}).
-\item Introducing your own types: how to define types that
- cannot be constructed with any of the basic methods
- ({\S}\ref{sec:adv-typedef}).
-\end{itemize}
-
-The material in this section goes beyond the needs of most novices.
-Serious users should at least skim the sections as far as type classes.
-That material is fairly advanced; read the beginning to understand what it
-is about, but consult the rest only when necessary.
-
-\index{pairs and tuples|(}
-\input{Pairs} %%%Section "Pairs and Tuples"
-\index{pairs and tuples|)}
-
-\input{Records} %%%Section "Records"
-
-
-\section{Type Classes} %%%Section
-\label{sec:axclass}
-\index{axiomatic type classes|(}
-\index{*axclass|(}
-
-The programming language Haskell has popularized the notion of type
-classes: a type class is a set of types with a
-common interface: all types in that class must provide the functions
-in the interface. Isabelle offers a similar type class concept: in
-addition, properties (\emph{class axioms}) can be specified which any
-instance of this type class must obey. Thus we can talk about a type
-$\tau$ being in a class $C$, which is written $\tau :: C$. This is the case
-if $\tau$ satisfies the axioms of $C$. Furthermore, type classes can be
-organized in a hierarchy. Thus there is the notion of a class $D$
-being a subclass\index{subclasses} of a class $C$, written $D
-< C$. This is the case if all axioms of $C$ are also provable in $D$.
-
-In this section we introduce the most important concepts behind type
-classes by means of a running example from algebra. This should give
-you an intuition how to use type classes and to understand
-specifications involving type classes. Type classes are covered more
-deeply in a separate tutorial \cite{isabelle-classes}.
-
-\subsection{Overloading}
-\label{sec:overloading}
-\index{overloading|(}
-
-\input{Overloading}
-
-\index{overloading|)}
-
-\input{Axioms}
-
-\index{type classes|)}
-\index{*class|)}
-
-\input{numerics} %%%Section "Numbers"
-
-\input{Typedefs} %%%Section "Introducing New Types"