Re: [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



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

Re: [isabelle-dev] The coming release of Isabelle2017

[Lars Hupel]

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