Re: [isabelle] [Isabelle2016-1-RC2] Proof outlines for induction proofs with several simultaneous goals
- To: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: Re: [isabelle] [Isabelle2016-1-RC2] Proof outlines for induction proofs with several simultaneous goals
- From: Makarius <makarius at sketis.net>
- Date: Sun, 4 Dec 2016 22:37:11 +0100
- In-reply-to: <firstname.lastname@example.org>
- References: <email@example.com> <firstname.lastname@example.org>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.5.1
On 11/11/16 14:24, Andreas Lochbihler wrote:
> Thanks for implementing proof outlines in Isabelle2016-1-RC2. I really
> find them useful. Unfortunately, they are not yet right for induction
> proofs with several goals.
> Are you aware of the problem?
I have not been aware of this particular problem, only of the general
observation that this new feature is somehow heuristic / partial. I will
improve on that eventually, but not for this release.
This archive was generated by a fusion of
Pipermail (Mailman edition) and