Impressum top_field.pvs

%------------------------------------------------------------------------------
% Mathematical Structures (Part II)
%
% Ring/Field-like Mathematical Structures with signatures:
%     [T:Type+,+,*:[T,T->T],zero:T]  or   [T:Type+,+,*:[T,T->T],zero,one:T]
%
%     Author: David Lester, Manchester University & NIA
%             Rick Butler
%
%     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
%------------------------------------------------------------------------------

top_field: THEORY

BEGIN
%----------------------------------------+------------------------------------
%             File                       | Mathematical Structure of *
%----------------------------------------+------------------------------------

    IMPORTING 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]
%             field_test

END top_field