Top File of PVS exact_real_arith Library

 
%------------------------------------------------------------------------------
% Top file for exact_real_arith
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            18/2/09   Initial Release Version
%------------------------------------------------------------------------------

top: THEORY

BEGIN

  IMPORTING prelude_aux,  % Various auxiliary results
            prelude_A4,   % Scaffolding for ...
            appendix,     % Approximation results
            prelude_sqrt, % Definition and properties of sqrt

            cauchy,       % Cauchy property
            int,          % int and nat definitions
            add,          % addition
            neg,          % negation
            sub,          % subtraction
            mul,          % multiplication
            inv,          % reciprocal
            div,          % division
            rat,          % Rationals
            shift,        % multiplication/division by 2^n
            min,          % min of two ERA numbers
            max,          % max of two ERA numbers
            sqrtx,        % sqrt of ERA
            power,        % raising an ERA to a natural power (x^n)
            sum,          % summation
            series,       % series
            powerseries,  % powerseries 
            atanx,        % arctangent of an ERA
            asinx,        % arcsine of an ERA
            acosx,        % arcosine of an ERA
            sincosx,      % sine and cosine of an ERA
            trigx,        % sec, cosec and cot
            log,          % log of an ERA
            exp,          % exp of an ERA
            hyperbolicx,  % hyperbolic functions
            test        

END top

The tag identifies links that are outside the NASA domain