src/HOL/ROOT
changeset 68510 795f39bfe4e1
parent 68445 c183a6a69f2d
child 68512 16ae55c77bcb
--- a/src/HOL/ROOT	Tue Jun 26 17:25:57 2018 +0200
+++ b/src/HOL/ROOT	Tue Jun 26 17:42:49 2018 +0200
@@ -58,7 +58,7 @@
   document_files "root.bib" "root.tex"
 
 session "HOL-Analysis" (main timing) in Analysis = HOL +
-  options [document_tags = "unimportant",
+  options [document_tags = "*=unimportant",
     document_variants = "document:manual=-proof,-ML,-unimportant"]
   sessions
     "HOL-Library"