On Thu, 14 Jan 2016, Florian Haftmann wrote:
Hi Thomas,
There is some interest here at Data61 (NICTA that was) in having a
localised record package in Isabelle-2016. I've done the initial
implementation and got the parts of the package I understand working
within locales etc, but something goes wrong with the code generation
aspect. Is there anyone who understands how to debug the code generator
who'd have time to look at that?
I am very sympathetic towards localized records, but this appears a too
major change to be done so shortly before the next release.
I am also interested in a properly localized record package, for about 7
years. Since it is so huge an complex, it still did not happen until
today.
The release train for Isabelle2016 is about to depart within a couple of
days, so it is pointless to consider changing anything there. As usual,
big changes happen *after* a release not before it. And even then, it can
take more than one release cycle to get it really through.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
