--- 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}