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

2016-01-14 Thread 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

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

2016-01-14 Thread Makarius
On Thu, 14 Jan 2016, Thomas Sewell wrote: Right. There was a plan here to investigate before the release, but the timing didn't work out. You mean *after* the release. Bigger changes are always reconsidered after lift-off of release N, to be included in release N + 1 or N + k for k >= 2.