src/HOL/ROOT
changeset 68445 c183a6a69f2d
parent 68443 43055b016688
child 68510 795f39bfe4e1
     1.1 --- a/src/HOL/ROOT	Tue Jun 12 16:09:12 2018 +0100
     1.2 +++ b/src/HOL/ROOT	Thu Jun 14 14:23:38 2018 +0100
     1.3 @@ -294,22 +294,16 @@
     1.4    theories
     1.5      (* Orders and Lattices *)
     1.6      Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)
     1.7 -
     1.8      (* Groups *)
     1.9      FiniteProduct        (* Product operator for commutative groups *)
    1.10      Sylow                (* Sylow's theorem *)
    1.11      Bij                  (* Automorphism Groups *)
    1.12 -    More_Group
    1.13 -    More_Finite_Product
    1.14      Multiplicative_Group
    1.15      Zassenhaus            (* The Zassenhaus lemma *)
    1.16 -
    1.17 -
    1.18      (* Rings *)
    1.19      Divisibility         (* Rings *)
    1.20      IntRing              (* Ideals and residue classes *)
    1.21      UnivPoly             (* Polynomials *)
    1.22 -    More_Ring
    1.23    document_files "root.bib" "root.tex"
    1.24  
    1.25  session "HOL-Auth" (timing) in Auth = "HOL-Library" +