--- 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
--- 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