[isabelle-dev] AFP: Session AVL-Trees broken

Lawrence Paulson lp15 at cam.ac.uk
Thu Nov 8 12:56:57 CET 2012

The long-term solution must be to deliver self-contained proof scripts, but obviously it will be difficult.

On 8 Nov 2012, at 11:51, Tjark Weber <webertj at in.tum.de> wrote:

> I've had the same experience before, while exchanging theories that
> heavily relied on sledgehammer with other people across different
> machines and prover versions: re-finding proofs is a brittle process.
> I am not sure whether that is an argument in favor of certificates, or
> what the best solution would be.

More information about the isabelle-dev mailing list