[isabelle-dev] NEWS: type-inference for object-logic

[Makarius]

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