\<subseteq> syntax for classes/classrel/axclass/instance;

--- a/doc-src/IsarRef/generic.tex	Mon Feb 12 20:43:12 2001 +0100
+++ b/doc-src/IsarRef/generic.tex	Mon Feb 12 20:44:02 2001 +0100
@@ -25,23 +25,24 @@
 \begin{rail}
   'axclass' classdecl (axmdecl prop comment? +)
   ;
-  'instance' (nameref '<' nameref | nameref '::' simplearity) comment?
+  'instance' (nameref ('<' | subseteq) nameref | nameref '::' simplearity) comment?
   ;
 \end{rail}
 
 \begin{descr}
-\item [$\AXCLASS~c < \vec c~axms$] defines an axiomatic type class as the
-  intersection of existing classes, with additional axioms holding.  Class
+\item [$\AXCLASS~c \subseteq \vec c~axms$] defines an axiomatic type class as
+  the intersection of existing classes, with additional axioms holding.  Class
   axioms may not contain more than one type variable.  The class axioms (with
   implicit sort constraints added) are bound to the given names.  Furthermore
   a class introduction rule is generated, which is employed by method
   $intro_classes$ to support instantiation proofs of this class.
   
-\item [$\INSTANCE~c@1 < c@2$ and $\INSTANCE~t :: (\vec s)c$] 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 augmented
-  by a type signature declaration corresponding to the resulting theorem.
+\item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)c$] 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
+  augmented by a type signature declaration corresponding to the resulting
+  theorem.
 \item [$intro_classes$] repeatedly expands all class introduction rules of
   this theory.  Note that this method usually needs not be named explicitly,
   as it is already included in the default proof step (of $\PROOFNAME$,

--- a/doc-src/IsarRef/isar-ref.tex	Mon Feb 12 20:43:12 2001 +0100
+++ b/doc-src/IsarRef/isar-ref.tex	Mon Feb 12 20:44:02 2001 +0100
@@ -18,6 +18,7 @@
 \newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
 \newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
 \newcommand{\isasymequiv}{\isamath{\equiv}}
+\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
 
 \railterm{percent,ppercent,underscore,lbrace,rbrace,atsign}
 \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}

--- a/doc-src/IsarRef/pure.tex	Mon Feb 12 20:43:12 2001 +0100
+++ b/doc-src/IsarRef/pure.tex	Mon Feb 12 20:44:02 2001 +0100
@@ -159,17 +159,18 @@
 \begin{rail}
   'classes' (classdecl comment? +)
   ;
-  'classrel' nameref '<' nameref comment?
+  'classrel' nameref ('<' | subseteq) nameref comment?
   ;
   'defaultsort' sort comment?
   ;
 \end{rail}
 
 \begin{descr}
-\item [$\isarkeyword{classes}~c<\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<c@2$] states a subclass relation between
-  existing classes $c@1$ and $c@2$.  This is done axiomatically!  The
+\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
+  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.
 \item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for

--- a/doc-src/IsarRef/syntax.tex	Mon Feb 12 20:43:12 2001 +0100
+++ b/doc-src/IsarRef/syntax.tex	Mon Feb 12 20:44:02 2001 +0100
@@ -159,10 +159,13 @@
 referring to the intersection of these classes.  The syntax of type arities is
 given directly at the outer level.
 
+\railalias{subseteq}{\isasymsubseteq}
+\railterm{subseteq}
+
 \indexouternonterm{sort}\indexouternonterm{arity}\indexouternonterm{simplearity}
 \indexouternonterm{classdecl}
 \begin{rail}
-  classdecl: name ('<' (nameref + ','))?
+  classdecl: name (('<' | subseteq) (nameref + ','))?
   ;
   sort: nameref
   ;