# HG changeset patch
# User haftmann
# Date 1157370932 -7200
# Node ID 210b326a03c95c75a285b91a581075e4bc565bda
# Parent  7c20ddbd911b148a927db5628bd29da0f147d5d2
some corrections in class section

diff -r 7c20ddbd911b -r 210b326a03c9 doc-src/IsarRef/generic.tex
--- 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}