To re-run the theory proofs, you will need to:

1.  Download the NASA Langley Research Center PVS Libraries for PVS 3.1 and the PVS strategies Manip and Field (all are obtainable in one tar file on the download page, and instructions are there, too).  If you already have downloaded the libraries, make sure they are up-to-date as they were updated in April, 2004.

2. Download the dump file of the PVS theories (an un-tarred verion is available here for browsing).

3. Unpack the file (tar -xzvf abstractions.tgz), and undump the file in PVS (M-x undump-pvs-files).  All files are imported by top.pvs, and comments appear therein as well.