[isabelle-dev] The coming release of Isabelle2017

Lawrence Paulson lp15 at cam.ac.uk
Sat Jul 8 23:28:42 CEST 2017

No, that’s precisely what I’d like to avoid. I prefer texts that you can actually read. It would be great to have something automatically generated, even if it needed manual tweaking (e.g. to rename variables).

And I’ve gone to some effort purging instances of “guess” from existing proofs.


> On 8 Jul 2017, at 22:16, Peter Lammich <lammich at in.tum.de> wrote:
> We already have proof goal_cases. Is that what you mean?

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170708/7d44d6cb/attachment-0002.html>

More information about the isabelle-dev mailing list