Top File of PVS analysis Library

 
top: THEORY
%------------------------------------------------------------------------
%
%    top_limits        -- Limit of a functions [T -> real] at a point  
%    top_sequence      -- Limits and operations on sequences of reals
%    top_continuity    -- Continuous functions [T -> real] 
%    top_derivative    -- Differential Calculus  
%    top_integral      -- Integral Calculus
%
%  See top_limits, top_sequences, top_continuity, top_derivative
%  for summary of contents
%
%      by Bruno Dutertre     Royal Holloway & Bedford New College
%         Rick Butler        NASA Langley Research Center
%         Cesar Munoz        National Institute For Aerospace
%         David Lester       Manchester University 
%         Anthony Narkawicz  NASA Langley Research Center
% 
%      Version 1.0    last modified 7/12/96
%      Version 1.1    updated to PVS 2.3   8/1/2000 by Rick Butler
%      Version 1.2    updated to PVS 2.3   3/1/2001 by Bruno in
%                     a slightly different way.
%                     Bruno ELIMINATED "const_fun" and associated
%                     conversion.  Now uses prelude "K_conversion".
%                     RWB added back "const_fun" definition to
%                     help with upward compatibility (real_fun_ops).
%
%                     Bruno changed "below_bounded" to "bounded_below?"
%                           and changed structure of its definition.
%                     Bruno changed "above_bounded" to "bounded_above?"
%                           and changed structure of its definition.
%      Version 1.3    Added theorem in derivatives_more 5/22/01
%      Version 1.4    put back "const_fun" for PVS2.4
%      Version 1.5    Used MACRO feature to rename all predicates
%                     in real_fun_preds, adding ? to name    2/28/02
%      Version 1.6    Added quadratic theory in "special_functions"  3/14/02
%      Version 1.7    quadratic theory moved to reals
%      Version 1.8    removed open? assugmption in integral theories 4/2/03
%      Version 1.9    removed duplicates with reals library 4/14/03
%      Version 2.0    proved step_function_integrable? in integral_step 
%      Version 2.1    ln_exp moved to lnexp library (12/8/03)
%      Version 2.2    David Lester added derivatives of inverse functions
%                     and derivative of sqrt
%      Version 2.3    NAME CHANGES -- See File NAME-CHANGES.txt
%      Version 2.4    ADDED integral_chg_var and integral_diff_doms
%      Version 2.5    NAME CHANGES: continuous2 --> cont_fun
%      Version 2.6    moved nth_derivatives, and taylors here from series
%      Version 2.7    add integration_by_parts and indefinite_integral 7/20/07
%      Version 2.8    metric spaces, compactness, uniform continuity
%
%  NOTE: top_integral relies on the Di Vito strategy package
%  NOTE: theories named  *_scaf are proof scaffolding, not intended for users
%------------------------------------------------------------------------
BEGIN

  IMPORTING top_limits, 
            top_sequences, 
            top_continuity,
            top_metric_spaces, 
            top_derivative,
	    top_riesz_representation,
            top_integral  %  requires Manip strategies

END top

The tag identifies links that are outside the NASA domain