[isabelle-dev] Yet another encounter with HOL-Word

[Gerwin Klein]

On 1 Mar 2014, at 9:00 am, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:

> I have the strong impression that the now existing infrastructure of
> quotient relations, transfer etc. would form a much more solid base than
> this adventurous low-level hacking.

Yes, that’s pretty much what I think Jeremy was trying to do back then when this infrastructure didn’t exist yet.


> But someone would have to take the burden and start to sort this out step by step.

Changing these is likely to break things, but not in a fundamental way. If someone has time to modernise this, I’m all for it.

Cheers,
Gerwin


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.