On 1 Mar 2014, at 9:00 am, Florian Haftmann <florian.haftm...@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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
