Re: [isabelle-dev] The coming release of Isabelle2017
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 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 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
Re: [isabelle-dev] The coming release of Isabelle2017
What I’m requesting requires no sophistication at all. It is merely to automate what we currently do by copying from one window and pasting to another, while inserting “fix”, “assume” and “show” in the obvious places. Larry > On 9 Jul 2017, at 16:32, Lars Hupel wrote: > > 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. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] The coming release of Isabelle2017
A while ago, Florian Haftmann sent a command that does something like this to the mailing list [1]. I attach a version that works with current Isabelle2016-1 (not sure if I got all the modifications right, but it seems to work at least on the example in the .thy file). Fabian [1] http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04443.html Explorer.thy Description: Binary data > Am 09.07.2017 um 16:58 schrieb Lawrence Paulson : > > What I’m requesting requires no sophistication at all. It is merely to > automate what we currently do by copying from one window and pasting to > another, while inserting “fix”, “assume” and “show” in the obvious places. > Larry > >> On 9 Jul 2017, at 16:32, Lars Hupel wrote: >> >> 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. > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev smime.p7s Description: S/MIME cryptographic signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
