* Pure: overloaded definitions are now actually checked for acyclic dependencies;

--- a/NEWS	Fri May 12 18:11:09 2006 +0200
+++ b/NEWS	Sat May 13 02:51:30 2006 +0200
@@ -37,6 +37,21 @@
 * Command 'no_translations' removes translation rules from theory
 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!
+
 * Isar: improper proof element 'guess' is like 'obtain', but derives
 the obtained context from the course of reasoning!  For example: