[isabelle-dev] Circular reasoning via multithreading seems too easy

Makarius makarius at sketis.net
Tue Dec 6 11:36:50 CET 2016

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.


More information about the isabelle-dev mailing list