Untitled Document

• PVS 3.2 Release Notes
  • Installation Notes
  • New Features
    • Startup Script Update
    • Theory Interpretation Enhancements
    • References to Mapped Entities
    • Cleaning up Specifications
    • Binary Files
    • Generating HTML
    • Default Strategies
    • Better handling of TCCs in Proofs
    • typepred! rule and all-typepreds strategy
    • grind-with-ext and reduce-with-ext
    • New forward chain commands
    • TeX Substitutions
    • add-declaration and IMPORTINGs
    • Prelude additions
  • Bug Fixes
    • Retypechecking
    • Quantifier Simplification
  • Incompatibilities
    • Ground Decision Procedure Completeness
    • Actuals not allowed for Current Theory
    • Referencing Library Theories
    • Renaming of Bound Variables
    • bddsimp and Enumeration Types
    • Prettyprinting Theory Instances
    • Assuming and Mapped Axiom TCC Visibility Rules
    • Replacing actuals including types
    • expand Rule uses Full Name
    • finite_sets min and max renamed
    • induct no longer beta-reduces everything

This document was generated on 4 November 2004 using texi2html 1.56k.