--- a/doc-src/IsarRef/generic.tex Mon Sep 04 08:18:00 2006 +0200
+++ b/doc-src/IsarRef/generic.tex Mon Sep 04 13:55:32 2006 +0200
@@ -105,7 +105,7 @@
\subsection{Axiomatic type classes}\label{sec:axclass}
-\indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{intro-classes}
+\indexisarcmd{axclass}\indexisarmeth{intro-classes}
\begin{matharray}{rcl}
\isarcmd{axclass} & : & \isartrans{theory}{theory} \\
\isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
@@ -470,13 +470,14 @@
\end{warn}
-\subsubsection{Classes}
+\subsubsection{Constructive type classes}
-A special case of locales are type classes. Type classes
+A special case of locales are constructive type classes.
+Constructive type classes
consist of a locale with \emph{exactly one} type variable
and an corresponding axclass.
-\indexisarcmd{class}\indexisarcmd{print-classes}
+\indexisarcmd{instance}\indexisarcmd{class}\indexisarcmd{print-classes}
\begin{matharray}{rcl}
\isarcmd{class} & : & \isartrans{theory}{local{\dsh}theory} \\
\isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
@@ -505,7 +506,7 @@
\item [$\CLASS~c = superclasses~+~body$] defines a new class $c$,
inheriting from $superclasses$. Simultaneously, a locale
- named $c$ is introduces, inheriting from the locales
+ named $c$ is introduced, inheriting from the locales
corresponding to $superclasses$; also, an axclass
named $c$, inheriting from the axclasses corresponding to
$superclasses$. $\FIXESNAME$ in $body$ are lifted
@@ -526,6 +527,8 @@
After finishing the proof, the theory will be
augmented by a type signature declaration corresponding to the
resulting theorems.
+ Note that this $\isarcmd{instance}$ command is different
+ from primitive axclass $\isarcmd{instance}$ (see \ref{sec:axclass}).
\item [$\INSTANCE~c \subseteq \vec{c}$] sets up a
goal stating
@@ -535,7 +538,7 @@
prove the additional class relation $c \subseteq \vec{c}$.
\item [$\isarkeyword{print_classes}$] prints the names of all classes
- in the current theory together with some additonal data.
+ in the current theory.
\end{descr}