[isabelle-dev] Localized record package [was: next release]

[Makarius]

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