*** General ***
* Type-inference improves sorts of newly introduced type variables for
the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL).
Thus terms like "f x" or "⋀x. P x" without any further syntactic context
produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare
INCOMPATIBILITY, need to provide explicit type constraints for Pure
types where this is really intended.
This refers to Isabelle/b41c1cb5e251. After approx. 20 years in the
pipeline, the change came out rather small, but it required a few rounds
of empirical studies to get to this point.
I have already made a routine check of the places where the improvement
stage now produces a different result. This is included in the above
change. For AFP it is only 61a1c5a37227.
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
