[isabelle-dev] Yet another encounter with HOL-Word
Gerwin.Klein at nicta.com.au
Sat Mar 1 01:02:33 CET 2014
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.
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.
More information about the isabelle-dev