OK, I'll respond to these points in-line.
A discussion without sources to look at is difficult.
OK, I attach my working version. Colleagues of mine were told off
recently for producing patches without the relevant authority, so these
days I begin these discussions in abstract. Feel free to
I have two items of interest for the coming release.
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
On Thu, 14 Jan 2016, Thomas Sewell wrote:
The second proposal is probably more contentious. I'm hoping to
reimplement a tool we had in the past that speeds up proof maintenance
work by selectively skipping proofs that are very likely to succeed. To
support that, I'm proposing adding a couple
I don't expect to contribute anything else before the next release. There are
little bits that I could add, but probably I should desist in the name of
stability.
Larry
___
isabelle-dev mailing list
isabelle-...@in.tum.de
