Top File of PVS extended_nnreal Library

 
%-------------------------------------------------------------------------
% top file for Extended nnreals
%
%     Author: David Lester, Manchester University
%
%     Version 1.0           20/08/07	Initial (DRL)
%-------------------------------------------------------------------------

top: THEORY

BEGIN

  IMPORTING code_product,       % A coding for diagonalizing a sequence
            double_index,       % double and single indexing for sequences
            double_nn_sequence, % Convergence properties of doubly indexed
                                % sequences of nnreals
            extended_nnreal     % The extended non-negative reals.

END top

The tag identifies links that are outside the NASA domain