Why ProofPower?
I am using ProofPower for the following reasons:
 I am familiar with it, having been involved in its development and application for many years.
 It is designed to work with the real logical characters rather then ascii equivalents.
 I like higher order logic, especially this variant.
The main claim to fame of ProofPower is its support for the Z specification language and the DERA compliance notation (for
refining Z to Ada), however, I'm not making any use of these.


ProofPower Documentation
For a full understanding of the specifications in ProofPower HOL you need to look at the semantics of HOL and at the theories
in the ancestry of the specification.
For the semantics of the language you can either look at the informal mathematical semantics which is available from Cambridge
for their system, or else at the formal specifications of ProofPower at the Lemma1 site.
For links to listings of the theories, see below.
This is a simple language, but precise semantics is never easy.

