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

2017-07-08 Thread Lawrence Paulson
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

2017-07-08 Thread Peter Lammich
We already have proof goal_cases. Is that what you mean?Peter Original Message Subject: Re: [isabelle-dev] The coming release of Isabelle2017From: Lawrence Paulson To: Markus Wenzel CC: isabelle-dev I am always using the new auto-complete facility for 	proof (cases “...”) and for induction. But could this be done for “proof" with any method, simply copying out the states of the subgoals? Then people would make a lot less use of “subgoals”, etc.
Larry


On 5 Jul 2017, at 21:04, Makarius  wrote:Is there anything else to take into account for this late-summer releaseprocess?___
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

2017-07-08 Thread Lawrence Paulson
I am always using the new auto-complete facility for 

proof (cases “...”) 

and for induction. But could this be done for “proof" with any method, simply 
copying out the states of the subgoals? Then people would make a lot less use 
of “subgoals”, etc.

Larry

> On 5 Jul 2017, at 21:04, Makarius  wrote:
> 
> Is there anything else to take into account for this late-summer release
> process?

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev