Re: [isabelle-dev] The coming release of Isabelle2017
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 Lammichwrote: > > 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
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, Makariuswrote: > > 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