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