A while ago, Florian Haftmann sent a command that does something like this to
the mailing list . 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).
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.
>> 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
Description: S/MIME cryptographic signature
isabelle-dev mailing list