157 \end{matharray} |
157 \end{matharray} |
158 |
158 |
159 \begin{rail} |
159 \begin{rail} |
160 'classes' (classdecl comment? +) |
160 'classes' (classdecl comment? +) |
161 ; |
161 ; |
162 'classrel' nameref '<' nameref comment? |
162 'classrel' nameref ('<' | subseteq) nameref comment? |
163 ; |
163 ; |
164 'defaultsort' sort comment? |
164 'defaultsort' sort comment? |
165 ; |
165 ; |
166 \end{rail} |
166 \end{rail} |
167 |
167 |
168 \begin{descr} |
168 \begin{descr} |
169 \item [$\isarkeyword{classes}~c<\vec c$] declares class $c$ to be a subclass |
169 \item [$\isarkeyword{classes}~c \subseteq \vec c$] declares class $c$ to be a |
170 of existing classes $\vec c$. Cyclic class structures are ruled out. |
170 subclass of existing classes $\vec c$. Cyclic class structures are ruled |
171 \item [$\isarkeyword{classrel}~c@1<c@2$] states a subclass relation between |
171 out. |
172 existing classes $c@1$ and $c@2$. This is done axiomatically! The |
172 \item [$\isarkeyword{classrel}~c@1 \subseteq c@2$] states a subclass relation |
|
173 between existing classes $c@1$ and $c@2$. This is done axiomatically! The |
173 $\INSTANCE$ command (see \S\ref{sec:axclass}) provides a way to introduce |
174 $\INSTANCE$ command (see \S\ref{sec:axclass}) provides a way to introduce |
174 proven class relations. |
175 proven class relations. |
175 \item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for |
176 \item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for |
176 any type variables given without sort constraints. Usually, the default |
177 any type variables given without sort constraints. Usually, the default |
177 sort would be only changed when defining new object-logics. |
178 sort would be only changed when defining new object-logics. |