[isabelle-dev] AFP: Session AVL-Trees broken
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