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
close_derivation/name_derivation).
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.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
