--- a/doc-src/IsarRef/Thy/Spec.thy Wed May 06 16:01:05 2009 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy Wed May 06 16:01:05 2009 +0200
@@ -752,7 +752,11 @@
text {*
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 @{text "c :: \<alpha> decl"} may be
+ defined separately on type instances
+ @{text "c :: (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t decl"}
+ for each type constructor @{text t}. At most occassions
overloading will be used in a Haskell-like fashion together with
type classes by means of @{command "instantiation"} (see
\secref{sec:class}). Sometimes low-level overloading is desirable.
@@ -782,7 +786,8 @@
A @{text "(unchecked)"} 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}
@@ -1065,10 +1070,7 @@
\end{itemize}
- Overloading means that a constant being declared as @{text "c :: \<alpha>
- decl"} may be defined separately on type instances @{text "c ::
- (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t decl"} for each type constructor @{text
- 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 @{text "\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n"}. Incomplete
specification patterns impose global constraints on all occurrences,
--- a/doc-src/IsarRef/Thy/document/Spec.tex Wed May 06 16:01:05 2009 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Wed May 06 16:01:05 2009 +0200
@@ -759,7 +759,11 @@
%
\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.
@@ -788,7 +792,8 @@
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}%
@@ -1092,7 +1097,7 @@
\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,