[isabelle-dev] AFP: Session AVL-Trees broken
makarius at sketis.net
Mon Dec 3 11:02:46 CET 2012
On Thu, 8 Nov 2012, Lawrence Paulson wrote:
> The long-term solution must be to deliver self-contained proof scripts,
> but obviously it will be difficult.
Self-contained as a "black-box binary" should be possible, but then it
becomes difficult to maintain theories: slight changes in the
specifications might cause big changes in the recovery of proofs.
For Z3 in particular, there is also the problem that you have to be a
non-commercial user to run it. This is hypothetical at the moment, since
there are no commercial Isabelle or AFP maintainers.
More information about the isabelle-dev