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

[Makarius]

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.


 	Makarius