* 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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
