PVS 2.4 patchlevel 1 is now available. It replaces PVS 2.4 Download it here.

This is primarily a bug fix. Only a few new features have been added. All bugs reported between Nov 25 and Dec 18, 2001 have been fixed. In addition,

• The check for legal assumings has been improved, and the Language Manual, Section 6.5. has been updated accordingly.
• The release notes are now included in the lib subdirectory, and may be viewed using M-x pvs-release-notes (C-c C-h r).
• The ndiv function has been generalized in the prelude to take an integer argument rather than a nat, and a JUDGEMENT provided for the nat case.