* Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;
authorwenzelm
Sun Aug 12 19:00:58 2007 +0200 (2007-08-12)
changeset 242344714e04fb8e9
parent 24233 5bec1b4149e7
child 24235 aea5c389a2f5
* Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;
NEWS
     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