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.m
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
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
