src/HOL/Algebra/Algebra.thy
changeset 70027 94494b92d8d0
parent 68582 b9b9e2985878
child 70040 6a9e2a82ea15
equal deleted inserted replaced
70019:095dce9892e8 70027:94494b92d8d0
     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
     4   imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Elementary_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