[isabelle-dev] NEWS: simultaneous sort constraints

[Makarius]

* Sort constraints are now propagated in simultaneous statements, just
like type constraints.  INCOMPATIBILITY in rare situations, where
distinct sorts used to be assigned accidentally.  For example:

   lemma "P (x::'a::foo)" and "Q (y::'a::bar)"  -- "now illegal"

   lemma "P (x::'a)" and "Q (y::'a::bar)"
     -- "now uniform 'a::bar instead of default sort for first occurence (!)"

This refers to Isabelle/fca432074fb2


 	Makarius