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 +