[isabelle-dev] »real« considered harmful

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Fri Jun 5 23:18:01 CEST 2015

> Maybe we should resurrect the idea of using adhoc overloading for the
> "real" abbreviation.

The idea in itself is not bad, but I am reluctant to pull ad-hoc
overloading into the HOL theories itself.  There are still too many
dragons sitting in the dark.

> Florian, does your rework of the generic machinery for syntactic
> abbreviations include moving more of the adhoc overloading into HOL?

This work has not even started yet…



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150605/48cf5cff/attachment.sig>

More information about the isabelle-dev mailing list