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 <l...@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 <lamm...@in.tum.de> wrote:
>> We already have proof goal_cases. Is that what you mean?
isabelle-dev mailing list

Reply via email to