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

[Lawrence Paulson]

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

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.