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