src/HOL/Algebra/Algebra.thy

--- a/src/HOL/Algebra/Algebra.thy	Wed Apr 03 12:55:27 2019 +0100
+++ b/src/HOL/Algebra/Algebra.thy	Wed Apr 03 14:55:30 2019 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Algebra/Algebra.thy *)
 
 theory Algebra
-  imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Elementary_Groups
+  imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Product_Groups
      Divisibility Embedded_Algebras IntRing Sym_Groups Exact_Sequence Polynomials
 begin
 end