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.
Platform: Linux, Mac OS, Cygwin
Poly/ML version: 5.7 or later
Download link: https://github.com/RobArthan/pp-contrib