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 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?
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 of hooks to Pure/goal.ML, similar to the hook in Pure/Isar/toplevel.ML. One hook will allow the tool to install an oberver (context -> thm -> unit) for completed proofs. Another (context -> thm -> bool) will allow the tool to observe proofs as they commence, and to optionally recommend they be skipped. This second change essentially just gives the user a little more control, they could skip the proofs with skip_proofs anyway. Still, I'm sure it will provoke some interesting discussion. Cheers, Thomas. On 14/01/16 02:55, Lawrence Paulson wrote:
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 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev