# HG changeset patch
# User haftmann
# Date 1157715191 -7200
# Node ID c9bfc874488cee46afe59b2087ebb448706885bc
# Parent  98ba42f199952634ef50838b1ce34d48579cdb49
changed order of type classes and axclasses

diff -r 98ba42f19995 -r c9bfc874488c doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Thu Sep 07 20:12:08 2006 +0200
+++ b/doc-src/IsarRef/generic.tex	Fri Sep 08 13:33:11 2006 +0200
@@ -1,4 +1,3 @@
-
 \chapter{Generic tools and packages}\label{ch:gen-tools}
 
 \section{Theory specification commands}
@@ -103,59 +102,6 @@
 instantiation.
 
 
-\subsection{Axiomatic type classes}\label{sec:axclass}
-
-\indexisarcmd{axclass}\indexisarmeth{intro-classes}
-\begin{matharray}{rcl}
-  \isarcmd{axclass} & : & \isartrans{theory}{theory} \\
-  \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
-  intro_classes & : & \isarmeth \\
-\end{matharray}
-
-Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional}
-interface to type classes (cf.~\S\ref{sec:classes}).  Thus any object logic
-may make use of this light-weight mechanism of abstract theories
-\cite{Wenzel:1997:TPHOL}.  There is also a tutorial on using axiomatic type
-classes in Isabelle \cite{isabelle-axclass} that is part of the standard
-Isabelle documentation.
-
-\begin{rail}
-  'axclass' classdecl (axmdecl prop +)
-  ;
-  'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
-  ;
-\end{rail}
-
-\begin{descr}
-  
-\item [$\AXCLASS~c \subseteq \vec c~~axms$] defines an axiomatic type class as
-  the intersection of existing classes, with additional axioms holding.  Class
-  axioms may not contain more than one type variable.  The class axioms (with
-  implicit sort constraints added) are bound to the given names.  Furthermore
-  a class introduction rule is generated (being bound as
-  $c_class{\dtt}intro$); this rule is employed by method $intro_classes$ to
-  support instantiation proofs of this class.
-  
-  The ``axioms'' are stored as theorems according to the given name
-  specifications, adding the class name $c$ as name space prefix; the same
-  facts are also stored collectively as $c_class{\dtt}axioms$.
-  
-\item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)s$] setup a
-  goal stating a class relation or type arity.  The proof would usually
-  proceed by $intro_classes$, and then establish the characteristic theorems
-  of the type classes involved.  After finishing the proof, the theory will be
-  augmented by a type signature declaration corresponding to the resulting
-  theorem.
-
-\item [$intro_classes$] repeatedly expands all class introduction rules of
-  this theory.  Note that this method usually needs not be named explicitly,
-  as it is already included in the default proof step (of $\PROOFNAME$ etc.).
-  In particular, instantiation of trivial (syntactic) classes may be performed
-  by a single ``$\DDOT$'' proof step.
-
-\end{descr}
-
-
 \subsection{Locales and local contexts}\label{sec:locale}
 
 Locales are named local contexts, consisting of a list of declaration elements
@@ -482,10 +428,10 @@
 \end{warn}
 
 
-\subsection{Constructive type classes}
+\subsection{Type classes}
 
-A special case of locales are constructive type classes.
-Constructive type classes
+A special case of locales are type classes.
+Type classes
 consist of a locale with \emph{exactly one} type variable
 and an corresponding axclass.
 
@@ -555,6 +501,60 @@
 \end{descr}
 
 
+\subsection{Axiomatic type classes}\label{sec:axclass}
+
+\indexisarcmd{axclass}\indexisarmeth{intro-classes}
+\begin{matharray}{rcl}
+  \isarcmd{axclass} & : & \isartrans{theory}{theory} \\
+  \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
+  intro_classes & : & \isarmeth \\
+\end{matharray}
+
+Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional}
+interface to type classes (cf.~\S\ref{sec:classes}).  Thus any object logic
+may make use of this light-weight mechanism of abstract theories
+\cite{Wenzel:1997:TPHOL}.  There is also a tutorial on using axiomatic type
+classes in Isabelle \cite{isabelle-axclass} that is part of the standard
+Isabelle documentation.
+
+\begin{rail}
+  'axclass' classdecl (axmdecl prop +)
+  ;
+  'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
+  ;
+\end{rail}
+
+\begin{descr}
+  
+\item [$\AXCLASS~c \subseteq \vec c~~axms$] defines an axiomatic type class as
+  the intersection of existing classes, with additional axioms holding.  Class
+  axioms may not contain more than one type variable.  The class axioms (with
+  implicit sort constraints added) are bound to the given names.  Furthermore
+  a class introduction rule is generated (being bound as
+  $c_class{\dtt}intro$); this rule is employed by method $intro_classes$ to
+  support instantiation proofs of this class.
+  
+  The ``axioms'' are stored as theorems according to the given name
+  specifications, adding the class name $c$ as name space prefix; the same
+  facts are also stored collectively as $c_class{\dtt}axioms$.
+  
+\item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)s$] setup a
+  goal stating a class relation or type arity.  The proof would usually
+  proceed by $intro_classes$, and then establish the characteristic theorems
+  of the type classes involved.  After finishing the proof, the theory will be
+  augmented by a type signature declaration corresponding to the resulting
+  theorem.
+
+\item [$intro_classes$] repeatedly expands all class introduction rules of
+  this theory.  Note that this method usually needs not be named explicitly,
+  as it is already included in the default proof step (of $\PROOFNAME$ etc.).
+  In particular, instantiation of trivial (syntactic) classes may be performed
+  by a single ``$\DDOT$'' proof step.
+
+\end{descr}
+
+
+
 \section{Derived proof schemes}
 
 \subsection{Generalized elimination}\label{sec:obtain}