# HG changeset patch
# User haftmann
# Date 1246543572 -7200
# Node ID 0bf275fbe93ad0fefc3c6994512385345946349b
# Parent  edce86bf85213f5af56b572801bfce74713e1e55
instance arities can be simultaneous

diff -r edce86bf8521 -r 0bf275fbe93a doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Thu Jul 02 16:00:28 2009 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy	Thu Jul 02 16:06:12 2009 +0200
@@ -600,7 +600,7 @@
     ;
     'instance'
     ;
-    'instance' nameref '::' arity
+    'instance' (nameref + 'and') '::' arity
     ;
     'subclass' target? nameref
     ;
@@ -644,7 +644,7 @@
   concluded by an @{command_ref (local) "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 @{command "instance"} in an instantiation target body sets
diff -r edce86bf8521 -r 0bf275fbe93a doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Thu Jul 02 16:00:28 2009 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Thu Jul 02 16:06:12 2009 +0200
@@ -614,7 +614,7 @@
     ;
     'instance'
     ;
-    'instance' nameref '::' arity
+    'instance' (nameref + 'and') '::' arity
     ;
     'subclass' target? nameref
     ;
@@ -653,7 +653,7 @@
   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