[isabelle-dev] The coming release of Isabelle2017
hupel at in.tum.de
Sun Jul 9 17:32:19 CEST 2017
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.
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
>And I’ve gone to some effort purging instances of “guess” from existing
>> 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...
More information about the isabelle-dev