On 05/12/16 17:13, Ondřej Kunčar wrote:
> If you remove the call of the function Thm.name_derivation, the cycle gets
> caught. The function
> is internally used in Goal.prove_future. It seems that the promises of the
> theorem in question
> are dropped in the function but we don’t understand whether this was intended
> or not.
This is what I have explained already abstractly: there is a conceptual
conflict of proof futures vs. proof terms (via
Usually everything that is trivial or easy works properly in Isabelle.
Only hard problems are open, sometimes for years.
There might be a quick "fix", but such surgery usually degrades the
overall system quality. Isabelle development follows a different model.
isabelle-dev mailing list