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

[Peter Lammich]

We already have proof goal_cases. Is that what you mean? Peter -------- Original Message -------- Subject: Re: [isabelle-dev] The coming release of Isabelle2017 From: 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 <makar...@sketis.net> 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