Owner: RobArthan
Category: Sample code
Examples of specification and proof using ProofPower,
This is a selection of documents giving examples of specification and proof using ProofPower, supplementing the examples for ProofPower-HOL and ProofPower-Z supplied with the system itself. The examples are supplied as PDF documents for you to read and as source tarballs so that you can experiment with them using ProofPower.
Dependencies:
Platform: Linux, Mac OS, Cygwin
Poly/ML version: 5.7 or later
Licence:
Download link: https://github.com/RobArthan/pp-contrib
Project link: http://www.lemma-one.com/ProofPower/examples/examples.html