doc-src/IsarRef/Thy/document/Spec.tex

     ;
     'instantiation' (nameref + 'and') '::' arity 'begin'
     ;
     'instance'
     ;
-    'instance' nameref '::' arity
+    'instance' (nameref + 'and') '::' arity
     ;
     'subclass' target? nameref
     ;
     'instance' nameref ('<' | subseteq) nameref
     ;

   to sort \isa{s} at the particular type instance \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}.  A plain \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command in the
   target body poses a goal stating these type arities.  The target is
   concluded by an \indexref{local}{command}{end}\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}} command.
 
   Note that a list of simultaneous type constructors may be given;
-  this corresponds nicely to mutual recursive type definitions, e.g.\
+  this corresponds nicely to mutually recursive type definitions, e.g.\
   in Isabelle/HOL.
 
   \item \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} in an instantiation target body sets
   up a goal stating the type arities claimed at the opening \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}.  The proof would usually proceed by \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}, and then establish the characteristic theorems of
   the type classes involved.  After finishing the proof, the