# HG changeset patch
# User wenzelm
# Date 1148501630 -7200
# Node ID ceacd4422b97f4147597f9f0c19dd1043427438d
# Parent  69c71d40f8a856bc66da17a4aa26d0896d207124
tuned;

diff -r 69c71d40f8a8 -r ceacd4422b97 NEWS
--- a/NEWS	Wed May 24 22:04:06 2006 +0200
+++ b/NEWS	Wed May 24 22:13:50 2006 +0200
@@ -38,11 +38,11 @@
 syntax.
 
 * Overloaded definitions are now actually checked for acyclic
-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.
+dependencies.  The overloading scheme is slightly more general than
+that 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 versions of overloading -- at the discretion of the user!
 
 Polymorphic constants are represented via type arguments, i.e. the
 instantiation that matches an instance against the most general
@@ -50,10 +50,10 @@
 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".
+impose global constraints on all occurrences, e.g. c('a * 'a) on the
+LHS means that more general c('a * 'b) will be disallowed on the RHS.
+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: