'classrel': support multiple arguments;
authorwenzelm
Sat May 29 14:55:56 2004 +0200 (2004-05-29)
changeset 14817321ff6bf29d1
parent 14816 b77cebcd7e6e
child 14818 ad83019a66a4
'classrel': support multiple arguments;
doc-src/IsarRef/pure.tex
     1.1 --- a/doc-src/IsarRef/pure.tex	Sat May 29 14:54:58 2004 +0200
     1.2 +++ b/doc-src/IsarRef/pure.tex	Sat May 29 14:55:56 2004 +0200
     1.3 @@ -165,7 +165,7 @@
     1.4  \begin{rail}
     1.5    'classes' (classdecl +)
     1.6    ;
     1.7 -  'classrel' nameref ('<' | subseteq) nameref
     1.8 +  'classrel' (nameref ('<' | subseteq) nameref + 'and')
     1.9    ;
    1.10    'defaultsort' sort
    1.11    ;
    1.12 @@ -175,7 +175,7 @@
    1.13  \item [$\isarkeyword{classes}~c \subseteq \vec c$] declares class $c$ to be a
    1.14    subclass of existing classes $\vec c$.  Cyclic class structures are ruled
    1.15    out.
    1.16 -\item [$\isarkeyword{classrel}~c@1 \subseteq c@2$] states a subclass relation
    1.17 +\item [$\isarkeyword{classrel}~c@1 \subseteq c@2$] states subclass relations
    1.18    between existing classes $c@1$ and $c@2$.  This is done axiomatically!  The
    1.19    $\INSTANCE$ command (see \S\ref{sec:axclass}) provides a way to introduce
    1.20    proven class relations.