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