diff -r 1b9462304e1d -r c64319959bab src/HOL/ROOT --- a/src/HOL/ROOT Mon Jul 02 10:17:23 2018 +0200 +++ b/src/HOL/ROOT Mon Jul 02 14:41:35 2018 +0100 @@ -288,7 +288,7 @@ session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" + description {* - Author: Clemens Ballarin, started 24 September 1999 + Author: Clemens Ballarin, started 24 September 1999, and many others The Isabelle Algebraic Library. *} @@ -305,6 +305,8 @@ Divisibility (* Rings *) IntRing (* Ideals and residue classes *) UnivPoly (* Polynomials *) + (* Main theory *) + Algebra document_files "root.bib" "root.tex" session "HOL-Auth" (timing) in Auth = "HOL-Library" +