ProofPower is a suite of tools for specification and proof in HOL and Z.
ProofPower is distributed as an open source product under the GNU GPL.
ProofPower is also known as OpenProofPower.
See the ProofPower web pages for more information.
(c) Copyright Lemma 1 Ltd.