# HG changeset patch
# User haftmann
# Date 1241618465 -7200
# Node ID c13b0406c0392dacaab89d38fb8bbfe84529e625
# Parent  c1969f609bf759d3630866d1a1c42e05f3bf1a51
tuned description of overloading

diff -r c1969f609bf7 -r c13b0406c039 doc-src/IsarRef/Thy/Spec.thy
--- 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,
diff -r c1969f609bf7 -r c13b0406c039 doc-src/IsarRef/Thy/document/Spec.tex
--- 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,