diff -r 027a6f43e408 -r 31346d22bb54 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Sun Oct 15 19:51:19 2000 +0200
+++ b/doc-src/IsarRef/generic.tex	Sun Oct 15 19:51:56 2000 +0200
@@ -30,20 +30,18 @@
 \end{rail}
 
 \begin{descr}
-\item [$\isarkeyword{axclass}~c < \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, which is
-  employed by method $intro_classes$ to support instantiation proofs of this
-  class.
-
-\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t ::
-  (\vec s)c$] 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 [$\AXCLASS~c < \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, which is employed by method
+  $intro_classes$ to support instantiation proofs of this class.
+  
+\item [$\INSTANCE~c@1 < c@2$ and $\INSTANCE~t :: (\vec s)c$] 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.
 \end{descr}