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

Makarius makarius at sketis.net
Tue Apr 12 17:14:02 CEST 2016

On Tue, 12 Apr 2016, Peter Lammich wrote:

> 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!?

Yes, but old tools may get broken, if slightly more general types are 
expected. E.g. see the record simprocs in 


More information about the isabelle-dev mailing list