[isabelle-dev] NEWS

[Makarius]

* 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.