src/HOL/ROOT

     Sylow                (* Sylow's theorem *)
     Bij                  (* Automorphism Groups *)
     More_Group
     More_Finite_Product
     Multiplicative_Group
+    Zassenhaus            (* The Zassenhaus lemma *)
+
 
     (* Rings *)
     Divisibility         (* Rings *)
     IntRing              (* Ideals and residue classes *)
     UnivPoly             (* Polynomials *)