--- a/doc-src/IsarRef/generic.tex Fri Apr 16 20:34:41 2004 +0200
+++ b/doc-src/IsarRef/generic.tex Fri Apr 16 20:59:09 2004 +0200
@@ -22,7 +22,7 @@
\begin{rail}
'axclass' classdecl (axmdecl prop +)
;
- 'instance' (nameref ('<' | subseteq) nameref | nameref '::' simplearity)
+ 'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
;
\end{rail}
@@ -39,8 +39,8 @@
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{\dtt}axioms$.
-
-\item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)c$] setup a
+
+\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