--- a/doc-src/IsarRef/pure.tex Sat May 29 14:54:58 2004 +0200
+++ b/doc-src/IsarRef/pure.tex Sat May 29 14:55:56 2004 +0200
@@ -165,7 +165,7 @@
\begin{rail}
'classes' (classdecl +)
;
- 'classrel' nameref ('<' | subseteq) nameref
+ 'classrel' (nameref ('<' | subseteq) nameref + 'and')
;
'defaultsort' sort
;
@@ -175,7 +175,7 @@
\item [$\isarkeyword{classes}~c \subseteq \vec c$] declares class $c$ to be a
subclass of existing classes $\vec c$. Cyclic class structures are ruled
out.
-\item [$\isarkeyword{classrel}~c@1 \subseteq c@2$] states a subclass relation
+\item [$\isarkeyword{classrel}~c@1 \subseteq c@2$] states subclass relations
between existing classes $c@1$ and $c@2$. This is done axiomatically! The
$\INSTANCE$ command (see \S\ref{sec:axclass}) provides a way to introduce
proven class relations.