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

 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
 Isabelle/Pure's definitional schemes support certain forms of
-  overloading (see \secref{sec:consts}).  At most occassions
+  overloading (see \secref{sec:consts}).  Overloading means that a
+  constant being declared as \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ decl{\isachardoublequote}} may be
+  defined separately on type instances
+  \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isacharparenright}\ t\ decl{\isachardoublequote}}
+  for each type constructor \isa{t}.  At most occassions
   overloading will be used in a Haskell-like fashion together with
   type classes by means of \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} (see
   \secref{sec:class}).  Sometimes low-level overloading is desirable.
   The \hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}} target provides a convenient view for
   end-users.

   tools, using the names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} as reference to the
   corresponding constants.  The target is concluded by \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}.
 
   A \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks for
   the corresponding definition, which is occasionally useful for
-  exotic overloading.  It is at the discretion of the user to avoid
+  exotic overloading (see \secref{sec:consts} for a precise description).
+  It is at the discretion of the user to avoid
   malformed theory specifications!
 
   \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%

   provide definitional principles that can be used to express
   recursion safely.
 
   \end{itemize}
 
-  Overloading means that a constant being declared as \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ decl{\isachardoublequote}} may be defined separately on type instances \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isacharparenright}\ t\ decl{\isachardoublequote}} for each type constructor \isa{t}.  The right-hand side may mention overloaded constants
+  The right-hand side of overloaded definitions may mention overloaded constants
   recursively at type instances corresponding to the immediate
   argument types \isa{{\isachardoublequote}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isachardoublequote}}.  Incomplete
   specification patterns impose global constraints on all occurrences,
   e.g.\ \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymalpha}{\isachardoublequote}} on the left-hand side means that all
   corresponding occurrences on some right-hand side need to be an