1.1 --- a/doc-src/IsarRef/generic.tex	Mon Feb 12 20:43:12 2001 +0100
     1.2 +++ b/doc-src/IsarRef/generic.tex	Mon Feb 12 20:44:02 2001 +0100
     1.3 @@ -25,23 +25,24 @@
     1.4  \begin{rail}
     1.5    'axclass' classdecl (axmdecl prop comment? +)
     1.6    ;
     1.7 -  'instance' (nameref '<' nameref | nameref '::' simplearity) comment?
     1.8 +  'instance' (nameref ('<' | subseteq) nameref | nameref '::' simplearity) comment?
     1.9    ;
    1.10  \end{rail}
    1.11  
    1.12  \begin{descr}
    1.13 -\item [$\AXCLASS~c < \vec c~axms$] defines an axiomatic type class as the
    1.14 -  intersection of existing classes, with additional axioms holding.  Class
    1.15 +\item [$\AXCLASS~c \subseteq \vec c~axms$] defines an axiomatic type class as
    1.16 +  the intersection of existing classes, with additional axioms holding.  Class
    1.17    axioms may not contain more than one type variable.  The class axioms (with
    1.18    implicit sort constraints added) are bound to the given names.  Furthermore
    1.19    a class introduction rule is generated, which is employed by method
    1.20    $intro_classes$ to support instantiation proofs of this class.
    1.21    
    1.22 -\item [$\INSTANCE~c@1 < c@2$ and $\INSTANCE~t :: (\vec s)c$] setup a goal
    1.23 -  stating a class relation or type arity.  The proof would usually proceed by
    1.24 -  $intro_classes$, and then establish the characteristic theorems of the type
    1.25 -  classes involved.  After finishing the proof, the theory will be augmented
    1.26 -  by a type signature declaration corresponding to the resulting theorem.
    1.27 +\item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)c$] setup a
    1.28 +  goal stating a class relation or type arity.  The proof would usually
    1.29 +  proceed by $intro_classes$, and then establish the characteristic theorems
    1.30 +  of the type classes involved.  After finishing the proof, the theory will be
    1.31 +  augmented by a type signature declaration corresponding to the resulting
    1.32 +  theorem.
    1.33  \item [$intro_classes$] repeatedly expands all class introduction rules of
    1.34    this theory.  Note that this method usually needs not be named explicitly,
    1.35    as it is already included in the default proof step (of $\PROOFNAME$,