Top File of PVS series Library

 
top: THEORY
%----------------------------------------------------------------------------
%
% Infinite Series
%
% Author: Ricky W. Butler        11/01/00
%         David Lester           12/01/03   (generalizations)
%         (Manchester University)
% 
% CHANGES:
%
%     Version 1.0          -- 11/01/00
%     Version 1.1 (Lester) -- updated  nth_derivatives and taylors theories
%     Version 1.2          -- 7/8/04   proved axioms, major upgrade
%                                      new theory: taylor_series
%     Version 1.3          -- 1/5/05   update to analysis name changes%
%     Version 1.4          -- 3/22/06  simplified powerseq definition and
%                                      moved nth_derivatives and taylors
%                                      to analysis library
%     Version 1.5          -- 12/14/07 added series_lems, absconv theories
%     Version 1.6          -- 9/15/09  series_aux
%----------------------------------------------------------------------------
BEGIN

   IMPORTING series,               % definition + properies of infinite series
             series_lems,          % New basic theorems
             series_aux,           % more theorems from David Lester
             absconv_series,       % Absolute convergence
             power_series,         % definition + properies of power series
             trig_fun,             % definition of trigonometric functions
             trig_props,           % basic trig identities
             taylor_series,        % expansion into Taylor's series
             power_series_deriv,   % derivative of a power series 
             power_series_integ    % integral of a power series 

END top

The tag identifies links that are outside the NASA domain