diff -r cedf3480fdad -r 75129a73aca3 src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Jul 11 23:24:25 2018 +0100
+++ b/src/HOL/ROOT	Thu Jul 12 11:23:46 2018 +0200
@@ -58,7 +58,7 @@
   document_files "root.bib" "root.tex"
 
 session "HOL-Analysis" (main timing) in Analysis = HOL +
-  options [document_tags = "theorem%important,corollary%important,proposition%important,%unimportant",
+  options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
     document_variants = "document:manual=-proof,-ML,-unimportant"]
   sessions
     "HOL-Library"