src/HOL/Algebra/Algebra.thy

--- a/src/HOL/Algebra/Algebra.thy	Sun Feb 26 21:17:53 2023 +0000
+++ b/src/HOL/Algebra/Algebra.thy	Mon Feb 27 17:09:59 2023 +0000
@@ -3,6 +3,6 @@
 theory Algebra
   imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Free_Abelian_Groups
      Divisibility Embedded_Algebras IntRing Sym_Groups Exact_Sequence Polynomials Algebraic_Closure
-     Left_Coset
+     Left_Coset SimpleGroups SndIsomorphismGrp
 begin
 end