# HG changeset patch
# User wenzelm
# Date 1148500687 -7200
# Node ID 2401b1a3087fc72d4e157f390d73acdaa5569b01
# Parent  ee9c7fa80d210683ad1e523e4bc71a630dc191dc
Pure: update on overloaded defs;

diff -r ee9c7fa80d21 -r 2401b1a3087f NEWS
--- a/NEWS	Wed May 24 10:02:36 2006 +0200
+++ b/NEWS	Wed May 24 21:58:07 2006 +0200
@@ -38,19 +38,22 @@
 syntax.
 
 * Overloaded definitions are now actually checked for acyclic
-dependencies.  Overloading of some constant c :: 'a decl is restricted
-to schematic instances c :: ('b)t decl, for any type constructor t.
-The RHS may mention overloaded constants recursively at type instances
-corresponding to the immediate argument types 'b.  This scheme covers
-the disciplined overloading of Haskell98, although Isabelle does not
-demand an exact correspondence to type class and instance
-declarations.  There is an internal dependency graph of all overloaded
-and non-overloaded definitions, which ensures that the collection of
-interdependent constants in a theory can still be interpreted in terms
-of the basic logic.
-
-INCOMPATIBILITY, use ``defs (unchecked overloaded)'' to admit more
-exotic overloading schemes -- at the discretion of the user!
+dependencies.  The overloading scheme covers is slightly more general
+that the disciplined overloading of Haskell98, although Isabelle does
+not demand an exact correspondence to type class and instance
+declarations.  INCOMPATIBILITY, use ``defs (unchecked overloaded)'' to
+admit more exotic overloading schemes.
+
+Polymorphic constants are represented via type arguments, i.e. the
+instantiation that matches an instance against the most general
+declaration given in the signature.  For example, with the declaration
+c :: 'a => 'a => 'a, an instance c :: nat => nat => nat is represented
+as c(nat).  Overloading is essentially simultaneous structural
+recursion over such type arguments.  Incomplete specification patterns
+impose global constraints on all occurrences, e.g. defining c('a * 'a)
+means that general c('a * 'b) will be disallowed.  Command
+'print_theory' outputs the normalized system of recursive equations,
+see section "definitions".
 
 * Isar: improper proof element 'guess' is like 'obtain', but derives
 the obtained context from the course of reasoning!  For example:
diff -r ee9c7fa80d21 -r 2401b1a3087f doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Wed May 24 10:02:36 2006 +0200
+++ b/doc-src/IsarRef/pure.tex	Wed May 24 21:58:07 2006 +0200
@@ -264,15 +264,11 @@
 decl$ may be defined separately on type instances $c ::
 (\vec\beta)\,t\,decl$ for each type constructor $t$.  The RHS may
 mention overloaded constants recursively at type instances
-corresponding to the immediate argument types $\vec\beta$.  This
-scheme covers the disciplined overloading of Haskell98, although
-Isabelle does not demand an exact correspondence to type class and
-instance declarations.
-
-There is an internal dependency graph of all overloaded and
-non-overloaded definitions, which ensures that the collection of
-interdependent constants in a theory can still be interpreted in terms
-of the basic logic.
+corresponding to the immediate argument types $\vec\beta$.  Incomplete
+specification patterns impose global constraints on all occurrences,
+e.g. $d :: \alpha \times \alpha$ on the LHS means that all
+corresponding occurrences on some RHS need to be an instance of this,
+general $d :: \alpha \times \beta$ will be disallowed.
 
 \indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}\indexoutertoken{constdecl}
 \begin{matharray}{rcl}