NASA Langley PVS Libraries (Version 5.2.5)   

5.2.5 a few lemmas added to analysis
5.2.4 a few lemmas added to reals and vectors
5.2.3 a few lemmas added to trig and vectors,  vect2D_trunc theory added
5.2.2 added theories angles_2D, between_2D to vectors library  -- March 14, 2008
5.2.1 A few proofs were fixed  -- March 6, 2008

5.2 Changes (Feb 29, 2008)
--------------------------
   -- Add library "fs" which is just a holding place for theories that
      should be in finite_sets.  These will hopefully be moved there
      in the next release of PVS.

   -- moved abs_props and real_facts into reals library. NOTE
      (stop-rewrite "abs_0")  (stop-rewrite "abs_nat") may 
      be helpful in repairing broken proofs that use analysis library
      or reals@abs_lems.  Can also use AUTO_REWRITE- in theory.
      

5.1.5 --> added vectors_sign theories to vectors library

5.1.4 --> added cross_3D to vectors library, sigma over vector-valued
          functions  2-11-08

5.1 Changes (Jan 25, 2008)
--------------------------
    -- The product operator added to the reals and ints library.  A generic
       theory is provided in product.pvs, which is similar to sigma.pvs.
       The following theories provide additional theorems for specific domains:
       product_below, product_int, product_nat, product_posnat, product_upto
    -- An experimental alternate finite sequences library "fseqs" added to 
       structures library

5.0 Changes (Jan 11, 2008)
--------------------------
    -- The types of the inverse trig functions have been simplified -- no
       internal function calls

4.9 Changes (Jan 2, 2008)
---------------------------
    -- Number Theory library contents moved to ints
    -- ints library made more consistent with prelude

4.8 Changes (Dec 17, 2007)
---------------------------
    -- New Scott Library provided by David Lester of Manchester University
    -- New sigma_set library provided by David Lester of Manchester University
    -- New lemmas in series library about absolute convergence
    -- Improvements to algebra library -- factor groups added


4.7 Changes (Nov 20, 2007)
---------------------------
    -- improvements to atan_approx and trig_approx in trig_fnd library
    -- improvements to interval library (Interval-4.a)
    -- improvements to manip

4.6 Changes (Nov 8, 2007)
---------------------------

    -- Improved sigma definition (simpler) -- old_sigma* theories retained
       NOTE: this will break some proofs, but an extra (expand "sigma") or
       replacing (expand"sigma") with (rewrite "sigma_rew") often easily
       fixes the proofs

4.5 Changes (Nov 1, 2007)
---------------------------
    -- Add quad_minmax to reals library
    -- improved closest_approach* in vectors library

4.4 Changes (Sept 17, 2007)
---------------------------
    -- New topology library added
    -- Some new lemmas in trig_fnd
    -- A few additions to algebra libray

4.3 Changes (July 19, 2007)
---------------------------
    -- graphs library: Menger's Theorem now general due to Jon Sjogren


4.2 Changes (May 10, 2007)
---------------------------
    -- complex library updated by David Lester
    -- added co_structures library with Jerry James's sequence theories
    -- fixed unproved theorems in float (Munoz)
    -- proof in lnexp_fnd/hyperbolic repaired (Lester)

4.1 Changes (April 24, 2007)
---------------------------

    all proofs in complex library repaired by David Lester

4.0 Changes (Dec 8, 2006)
-------------------------

    updated to PVS 4.0

3.2.2 Changes (Mar 24, 2006)
-------------------------------

moved nth_derivatives, and taylors from series to analysis library.
simplified definition of 'powerseq" in series library.

3.2.1.9 Changes (Nov 30, 2005)
-------------------------------

restored float library

3.2.1.8 Changes (Oct 25, 2005)
-------------------------------

Removed IMPORTING reals@ in reals library that was causing
some problems.

3.2.1.7 Changes (Sept 15, 2005)
-------------------------------

Added new intervals library

3.2.1.6 Changes (July 19, 2005)
-------------------------------

A matroids and mappings theory was added to the graphs library. 

3.2.1.5 Changes (May 12, 2005)
------------------------------ 

NAME-CHANGES:
  composition_continuous1 -> composition_cont 
  composition_continuous2 -> composition_cont_set 
  composition_continuous3 -> composition_cont_fun 
  formatting in analysis
  update to sets_aux, orders


3.2.1.4 Changes (April 21, 2005)
-------------------------------- 
    Split sets_aux into sets_aux and an orders library
    fixed atan2_props

3.2.1.3 Changes 
--------------- 
    The directory lnexp now contains an axiomatic version.  
    The foundational version is in lnexp_fnd.

    trig -- updated to match foundational version (trig_fnd).

3.2.1.2 Changes
---------------
     float -- new library
     reals -- factorial props
     lnexp -- ln_exp_series_alt modified

3.2.1.1 Changes
-------------
     trig_fnd -- improvements to exp_approx, ln_approx, tan_approx,
                 trig_ineq, and trig_degree
     lnexp    -- theories ln_exp_series_alt, ln_exp_ineq added

3.2.1 Changes
-------------
    
     reals -- new theory: log_nat
     reals -- sqrt_approx updated
     lnexp -- ln_approx updated
     lnexp -- infinite series for ln added in theory ln_series
     series -- integral_powerseries theorem completed
     analysis -- integral_chg_var, integral_dif_doms added,
                 fundamental4 lemma added.