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
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.