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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
