[isabelle-dev] The coming release of Isabelle2017

[Lawrence Paulson]

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.

Larry

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