[isabelle-dev] The coming release of Isabelle2017

Lawrence Paulson lp15 at cam.ac.uk
Sat Jul 8 22:48:06 CEST 2017


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 <makarius at sketis.net> wrote:
> 
> Is there anything else to take into account for this late-summer release
> process?

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170708/23fa8342/attachment-0002.html>


More information about the isabelle-dev mailing list