Quelle  top_group.pvs

%------------------------------------------------------------------------------
% Mathematical Structures (Part I)
%
% Group-like Structures with signature [T:Type+,*:[T,T->T],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_group: THEORY

BEGIN

   IMPORTING groupoid,              
             commutative_groupoid,  
             monad,                 
             semigroup,             
             commutative_semigroup, 
             monoid,                
             cyclic_monoid,
             cyclic_group,
             group,           
             abelian_group,         
             symmetric_groups,
             group_test,


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

%            homomorphism_theorems   %% RWB breaks PVS 
%            cayleys                 %% RWB experimental

END top_group