Re: [isabelle] [Isabelle2016-1-RC2] Proof outlines for induction proofs with several simultaneous goals

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 MHonArc.