# HG changeset patch # User wenzelm # Date 1147481490 -7200 # Node ID 285771cec083346fb7c0611b3afcc7a6a4f2d7e1 # Parent 3b6629701a79eb839afa42ee8e8cdb4ba9aff192 * Pure: overloaded definitions are now actually checked for acyclic dependencies; diff -r 3b6629701a79 -r 285771cec083 NEWS --- 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: