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

Reply via email to