src/HOL/ROOT
changeset 65416 f707dbcf11e3
parent 65382 de848ac5e0d7
child 65417 fc41a5650fb1
--- a/src/HOL/ROOT	Thu Apr 06 22:04:30 2017 +0200
+++ b/src/HOL/ROOT	Thu Apr 06 08:33:37 2017 +0200
@@ -311,11 +311,15 @@
     FiniteProduct        (* Product operator for commutative groups *)
     Sylow                (* Sylow's theorem *)
     Bij                  (* Automorphism Groups *)
+    More_Group
+    More_Finite_Product
+    Multiplicative_Group
 
     (* Rings *)
     Divisibility         (* Rings *)
     IntRing              (* Ideals and residue classes *)
     UnivPoly             (* Polynomials *)
+    More_Ring
   document_files "root.bib" "root.tex"
 
 session "HOL-Auth" (timing) in Auth = HOL +