# HG changeset patch
# User wenzelm
# Date 1085835356 -7200
# Node ID 321ff6bf29d1a3f84a6b02ebd648aadd6fba252c
# Parent  b77cebcd7e6e18ed53789f14e54c8ae84b8ac39c
'classrel': support multiple arguments;

diff -r b77cebcd7e6e -r 321ff6bf29d1 doc-src/IsarRef/pure.tex
--- 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.