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