--- a/NEWS Sun Aug 12 18:53:05 2007 +0200
+++ b/NEWS Sun Aug 12 19:00:58 2007 +0200
@@ -46,6 +46,13 @@
feature, which will disappear eventually. Even now, the theory loader no
longer maintains dependencies on such files.
+* Syntax: the scope for resolving ambiguities via type-inference is now
+limited to individual terms, instead of whole simultaneous
+specifications as before. This greatly reduces the complexity of the
+syntax module and improves flexibility by separating parsing and
+type-checking. INCOMPATIBILITY: additional type-constraints (explicit
+'fixes' etc.) are required in rare situations.
+
* Legacy goal package: reduced interface to the bare minimum required
to keep existing proof scripts running. Most other user-level
functions are now part of the OldGoals structure, which is *not* open