Top File of PVS algebra Library

%------------------------------------------------------------------------------
% Mathematical Structures (algebra)
%
% Group-, Ring-, and Field-like Mathematical Structures.
%
%     Author: David Lester, Manchester University & NIA
%             Rick Butler,  NASA Langley
%
%
%     Version 1.0            3/1/02
%     Version 1.1           12/3/03   New library structure
%     Version 1.2            5/5/04   Reworked for definition files DRL
%     Version 1.3          10/18/04   Added a bunch of AUTO-REWRITE+s
%     Version 1.4           8/27/07   Added theory cyclic_groups
%     Version 1.5          12/14/07   Lagrange proof improved, cosets
%                                     factor_groups
%     Version 1.6          12/20/07   Consolidated finite_* theories into
%                                     main theories -- no need for parent type
%                                     to be finite. Can construct finite
%                                     groups from infinite domains, renamed
%                                     inverse -> inv for slow typers
%
%------------------------------------------------------------------------------

top: THEORY

BEGIN

IMPORTING top_group,
%---------------------
groupoid,
commutative_groupoid,
semigroup,
commutative_semigroup,
monoid,
cyclic_monoid,
cyclic_group,
group,
subgroups,
lagrange,
abelian_group,
symmetric_groups,
group_test,

finite_cyclic_groups,
infinite_cyclic_groups,
factor_groups,          %% RWB experimental
A_group,
homomorphisms,
cayleys,
zn,

top_field,
%---------------------------
ring,                      % semigroup[T,*]
commutative_ring,          % commutative_semigroup[T,*]
ring_nz_closed,            % semigroup[T,*], semigroup[nz_T,*]
ring_with_one,             % monoid[T,*,one]
commutative_ring_with_one, % commutative_monoid[T,*,one]
integral_domain,           % commutative_semigroup[T,*]
% commutative_semigroup[nz_T,*]
division_ring,             % monoid[T,*,one], group[nz_T,*,one]
field                      % commutative_monoid[T,*,one]
% abelian_group[nz_T,*,one]
END top

The tag identifies links that are outside the NASA domain