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