[isabelle-dev] The coming release of Isabelle2017

[Fabian Immler]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: Explorer.thy
Type: application/octet-stream
Size: 1784 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170709/99a97889/attachment-0002.obj>
-------------- next part --------------

> Am 09.07.2017 um 16:58 schrieb Lawrence Paulson <lp15 at cam.ac.uk>:
> 
> 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 <hupel at in.tum.de> 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4765 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170709/99a97889/attachment.bin>