[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 
http://isabelle.in.tum.de/repos/isabelle/diff/b41c1cb5e251/src/HOL/Tools/record.ML


 	Makarius



More information about the isabelle-dev mailing list