PVS 4.2 is now available - this mostly fixes bug relating to recursive judgements and theory interpretations - for more details see the release notes at http://pvs.csl.sri.com/pvs-release-notes/pvs-release-notes.html As usual, please let us know of any bugs or new features you would like to see, and feel free to contribute to the PVS wiki. at http://pvs-wiki.csl.sri.com Regards, Sam Owre