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

Makarius 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 mailing list