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

[Peter Lammich]

Nice one,

so we're not going to see the annoying "... not of sort 'type'" error
any more, which used to occur occasionally in Isabelle/HOL
developments!?

--
  Peter

On Di, 2016-04-12 at 16:46 +0200, Makarius wrote:
> *** 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev