# HG changeset patch
# User wenzelm
# Date 982007042 -3600
# Node ID 34d58b1818f4c0f2d6f8916b87ae5b22c1c96ac1
# Parent  b301d1f725524f1d53faa3d0269f214acbf9f3dc
\<subseteq> syntax for classes/classrel/axclass/instance;

diff -r b301d1f72552 -r 34d58b1818f4 doc-src/IsarRef/generic.tex
--- 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$,
diff -r b301d1f72552 -r 34d58b1818f4 doc-src/IsarRef/isar-ref.tex
--- 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}
diff -r b301d1f72552 -r 34d58b1818f4 doc-src/IsarRef/pure.tex
--- 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
diff -r b301d1f72552 -r 34d58b1818f4 doc-src/IsarRef/syntax.tex
--- 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
   ;