[isabelle-dev] NEWS

Makarius makarius at sketis.net
Sun Aug 12 19:01:41 CEST 2007

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

More information about the isabelle-dev mailing list