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

Reply via email to