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