Re: [isabelle] recdef problem

Elsa L Gunter wrote:

It would be nice if someone (more knowledgable of the inner workings of Isabelle than I currently am) would modify the redef procedure so that instead of failing with "bad final proof state" it would behave like the instance procedure and throw you into proving the "bad final proof state".

This is a problem I started working on, but it will certainly not make it into the next release. So the workaround Elsa described is currently the way to go... but there is hope for the future.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.