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 <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 >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 <lamm...@in.tum.de> wrote: >> >> We already have proof goal_cases. Is that what you mean?
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
