[isabelle-dev] Localized record package [was: next release]
makarius at sketis.net
Thu Jan 14 14:47:51 CET 2016
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
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.
More information about the isabelle-dev