[isabelle-dev] The coming release of Isabelle2017

[Lars Hupel]

I currently supervise a student who's investigating proof refactoring. One possible outcome of this would be a tool that also does what you suggested. It's a little too early to tell, though.

Cheers
Lars

On 8 July 2017 23:28:42 CEST, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
>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/20170709/95487504/attachment-0002.html>