Although working with Poly/ML is recommended, any (less-trusting) users building on theories of others may wish to check, by running with both compilers, that the supplied proof scripts do not exploit compiler-specific loopholes to circumvent proof.
Anyone following the Isabelle mailing list recently will note that this provides little additional assurance when operating in a zero-trust environment: running with both compilers only helps with item 2d on Mark's list:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-January/msg00085.html Still, every little helps... Phil
Description: GNU Zip compressed data
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com