## Top File of PVS scott Library

```
%------------------------------------------------------------------------------
% Top for Scott Topology
%
% All references are to BA Davey and HA Priestly "Introduction to Lattices and
% Orders", CUP, 1990.
%
% This library defines the Scott Topology, and shows that continuous functions
% are increasing and lub-preserving; and -- under pointwise-ordering -- also
% form a Scott Topology.
%
% The main reason Computer Scientists are interested is that it constitutes a
% general foundation on which to build the fixpoint theory needed for the
% semantics of loops or recursion.
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
%     Version 1.0            25/12/07  Initial Version
%------------------------------------------------------------------------------

top: THEORY

BEGIN

IMPORTING
partial_function_props,       % Easy-to-use partial function properties
scott,                        % Definition of Scott Topology
scott_continuity,             % Definition of Continuity
pointwise_orders_aux,         % Extras for continuous pointwise orders
scott_identity_continuity,    % Identity is scott continuous
scott_composition_continuity, % Composition is scott continuous
fixpoints,                    % Definition of Fixpoints
admissible,                   % Fixpoint induction
dual_fixpoints,               % Fixpoint Induction over two types
scott_product

% Extras for orders library %% INTEGRATED %%
%
%     bounded_orders_aux,     % Extras for orders@bounded_orders
%     ordered_subset_aux,     % Extras for orders@ordered_subset
%
% New Theory files for orders library  %% MOVED %%
%
%     lift_props,             % Extras for the lift datatype
%     directed_orders,        % New theories for orders library
%     bounded_order_props,    % Properties of bounded orders
%     directed_order_props,   % Properties of directed orders
%     partial_order_props,    % Properties of partial orders
%     partial_order_lift
%     lifted_orders,          % Induced properties of lifted orders
%     sum_orders,             % Induced properties of union orders
%     product_orders          % Induced properties of product orders

END top
```
The tag identifies links that are outside the NASA domain