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, M
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 in
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.
Larr
