[isabelle-dev] »real« considered harmful

[Florian Haftmann]

> 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…

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

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