Details About PVS Calculus Library

% Formal Methods Team
% ICASE - NASA Langley
%
%   C. Munoz     (munoz@icase.edu) 
%   G. Dowek     (gilles.dowek@inria.fr)
%   R. Butler    (R.W.Butler@larc.nasa.gov)
%
% Version 1.1   (May 21, 2001)
% Version 1.2   (Feb 26, 2002)   See real_fun_preds
% Version 1.3   (Apr 14, 2003)   Removed duplicate theories
% Version 1.4   (Jul 28, 2004)   Added integral calculus stuff 
%
% Developed using Dutertre's real analysis library.  The goal was
% to provide a compact, easy-to-use calculus theory for functions
% from [real -> real]. Once PVS 3 is released, this library will be 
% formally shown to be consistent.  Currently the soundness of this
% library is based upon a syntactic comparison with the analysis 
% library.

%  The following theories were created by copying sections from 
%  the analysis library and changing lemmas into axioms.
%
%          chain_rule_ax.pvs
%          continuous_functions_ax.pvs
%          derivative_props_ax.pvs
%          derivatives_ax.pvs
%          intermediate_value_ax.pvs
%          restriction_continuous_ax.pvs
%          real_fun_props_ax.pvs 
%
% NOTE: User's of this library can quickly switch to the analysis
% library by changing the IMPORTINGS in "derivatives_con" and "extra_con".
% See comments in these theories.
% 
%
%------------------------------------------------------------------------------
BEGIN

  IMPORTING calculus,                  % basic properties of derivatives
                                       % of functions [real -> real]

%                derivatives_ax[T], 
%                chain_rule_ax,
%                deriv_sqrt,
%                deriv_trig,



            calculus_extra,             % additional properties such as
                                        % mean value theorem

%                continuous_functions_ax,
%                intermediate_value_ax,  
%                restriction_continuous_ax,
%                derivative_props_ax    

%                 ln_exp_ax,             % provide ln and exp functions
%                 expt_ax,               % provide generalized expt function

                 integral_ax,         
                 fundamental_ax