PVS 3.0 release notes

• Overview
• New Features
  • Allegro 6.2 port
  • Theory Interpretations
  • Multiple Proofs
  • Better Library Support
  • Cotuples
  • Coinduction
  • Datatype Updates
  • Datatype Additions
  • Conversion Extensions
  • Conversion Messages
  • More TCC Information
  • Show Declaration TCCs
  • Numbers as Constants
  • Theory Search
  • Improved Decision Procedures
  • ICS Integration
  • LET Reduce
  • Prelude Changes
    • New Theories
    • New Declarations
    • Modified Declarations
  • Conversion Expressions
  • Judgement TCC proofs
  • PVS Startup Change
  • Dump File Change
  • Bitvector Library
• Bug Fixes
• Incompatibilities
  • Improved Decision Procedures
  • Prelude Changes
  • Theory Abbreviations
  • Conversion Expressions
  • Occurrence numbers in expand proof command

This document was generated on 19 December 2002 using texi2html 1.56k.