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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
