src/HOL/Algebra/Algebra.thy
changeset 70063 adaa0a6ea4fe
parent 70040 6a9e2a82ea15
child 70160 8e9100dcde52
equal deleted inserted replaced
70045:7b6add80e3a5 70063:adaa0a6ea4fe
     1 (*  Title:      HOL/Algebra/Algebra.thy *)
     1 (*  Title:      HOL/Algebra/Algebra.thy *)
     2 
     2 
     3 theory Algebra
     3 theory Algebra
     4   imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Product_Groups
     4   imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Free_Abelian_Groups
     5      Divisibility Embedded_Algebras IntRing Sym_Groups Exact_Sequence Polynomials
     5      Divisibility Embedded_Algebras IntRing Sym_Groups Exact_Sequence Polynomials
     6 begin
     6 begin
     7 end
     7 end