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

Makarius 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 mailing list