Details About PVS Reals Library

   top_sigma,         % set of summation theories
   product_real,      % product of a function
   bounded_reals,     % defines sup, inf, max, min
   real_sets,         % more properties of bounded sets of reals
   abs_lems,          % additional properties about absolute value
   exponent_props,    % additional properties of expt
   sqrt,              % non-axiomatic version of sqrt
   log_nat,           % Natural and real part of a logarithm 
                      %   (Requires Manip+Field)
   sqrt_approx,       % approximation to sqrt
                      %   (Requires Manip+Field)
   sqrt_rew,          % auto-rewrites for sqrt
   real_fun_ops,      % adding, subtracting, etc on functions
   real_fun_preds,    % increasing?, decreasing?, etc on functions
   real_fun_props,    % properties about defs in real_fun_preds
   sign,              % properties of the sign function
   factorial,         % factorial function
   factorial_props,   % additional properties of factorial function
   quadratic,         % Solution of quadratic equations
   quadratic_minmax,  % Minimum and Maximum of quadratic equations
   quad_minmax,       % easier to use quadratic_minmax
   binomial,          % Binomial coefficient       
   polynomials,       % polynomials
   harmonic_polynomials,
   circles_and_lines