diff -r 813a08dff3fd -r beeebae99746 src/Doc/ROOT
--- a/src/Doc/ROOT	Wed May 19 13:19:37 2021 +0200
+++ b/src/Doc/ROOT	Wed May 19 13:21:08 2021 +0200
@@ -1,7 +1,7 @@
 chapter Doc
 
 session Classes (doc) in "Classes" = HOL +
-  options [document_logo = "Isar", document_build = "build",
+  options [document_logo = "Isar", document_bibliography, document_build = "build",
     document_variants = "classes", quick_and_dirty]
   theories [document = false] Setup
   theories Classes
@@ -18,7 +18,7 @@
     "style.sty"
 
 session Codegen (doc) in "Codegen" = HOL +
-  options [document_logo = "Isar", document_build = "build",
+  options [document_logo = "Isar", document_bibliography, document_build = "build",
     document_variants = "codegen", print_mode = "no_brackets,iff"]
   sessions
     "HOL-Library"
@@ -46,7 +46,7 @@
     "style.sty"
 
 session Corec (doc) in "Corec" = Datatypes +
-  options [document_build = "build", document_variants = "corec"]
+  options [document_build = "build", document_bibliography, document_variants = "corec"]
   theories
     Corec
   document_files (in "..")
@@ -62,7 +62,7 @@
     "style.sty"
 
 session Datatypes (doc) in "Datatypes" = HOL +
-  options [document_build = "build", document_variants = "datatypes"]
+  options [document_build = "build", document_bibliography, document_variants = "datatypes"]
   sessions
     "HOL-Library"
   theories [document = false]
@@ -82,7 +82,7 @@
     "style.sty"
 
 session Eisbach (doc) in "Eisbach" = HOL +
-  options [document_logo = "Eisbach", document_build = "build",
+  options [document_logo = "Eisbach", document_bibliography, document_build = "build",
     document_variants = "eisbach", quick_and_dirty,
     print_mode = "no_brackets,iff", show_question_marks = false]
   sessions
@@ -107,7 +107,7 @@
     "style.sty"
 
 session Functions (doc) in "Functions" = HOL +
-  options [document_build = "build", document_variants = "functions",
+  options [document_build = "build", document_bibliography, document_variants = "functions",
     skip_proofs = false, quick_and_dirty]
   theories Functions
   document_files (in "..")
@@ -134,7 +134,8 @@
     "prelude.tex"
 
 session Intro (doc) in "Intro" = Pure +
-  options [document_logo = "_", document_build = "build", document_variants = "intro"]
+  options [document_logo = "_", document_bibliography, document_build = "build",
+    document_variants = "intro"]
   document_files (in "..")
     "prepare_document"
     "pdfsetup.sty"
@@ -150,7 +151,7 @@
     "root.tex"
 
 session Implementation (doc) in "Implementation" = HOL +
-  options [document_logo = "Isar", document_build = "build",
+  options [document_logo = "Isar", document_bibliography, document_build = "build",
     document_variants = "implementation", quick_and_dirty]
   theories
     Eq
@@ -179,8 +180,8 @@
     "style.sty"
 
 session Isar_Ref (doc) in "Isar_Ref" = HOL +
-  options [document_logo = "Isar", document_build = "build", document_variants = "isar-ref",
-    quick_and_dirty, thy_output_source]
+  options [document_logo = "Isar", document_bibliography, document_build = "build",
+    document_variants = "isar-ref", quick_and_dirty, thy_output_source]
   sessions
     "HOL-Library"
   theories
@@ -215,7 +216,7 @@
     "style.sty"
 
 session JEdit (doc) in "JEdit" = HOL +
-  options [document_logo = "jEdit", document_build = "build",
+  options [document_logo = "jEdit", document_bibliography, document_build = "build",
     document_variants = "jedit", thy_output_source]
   theories
     JEdit
@@ -253,7 +254,7 @@
     "theories.png"
 
 session Sugar (doc) in "Sugar" = HOL +
-  options [document_build = "build", document_variants = "sugar"]
+  options [document_build = "build", document_bibliography, document_variants = "sugar"]
   sessions
     "HOL-Library"
   theories Sugar
@@ -266,8 +267,8 @@
     "root.tex"
 
 session Locales (doc) in "Locales" = HOL +
-  options [document_build = "build", document_variants = "locales",
-    thy_output_margin = 65, skip_proofs = false]
+  options [document_build = "build", document_bibliography,
+    document_variants = "locales", thy_output_margin = 65, skip_proofs = false]
   theories
     Examples1
     Examples2
@@ -281,7 +282,8 @@
     "root.tex"
 
 session Logics (doc) in "Logics" = Pure +
-  options [document_logo = "_", document_build = "build", document_variants = "logics"]
+  options [document_logo = "_", document_bibliography, document_build = "build",
+    document_variants = "logics"]
   document_files (in "..")
     "prepare_document"
     "pdfsetup.sty"
@@ -300,7 +302,7 @@
     "syntax.tex"
 
 session Logics_ZF (doc) in "Logics_ZF" = ZF +
-  options [document_logo = "ZF", document_build = "build",
+  options [document_logo = "ZF", document_bibliography, document_build = "build",
     document_variants = "logics-ZF", print_mode = "brackets", thy_output_source]
   sessions
     FOL
@@ -334,7 +336,8 @@
     "root.tex"
 
 session Nitpick (doc) in "Nitpick" = Pure +
-  options [document_logo = "Nitpick", document_build = "build", document_variants = "nitpick"]
+  options [document_logo = "Nitpick", document_bibliography, document_build = "build",
+    document_variants = "nitpick"]
   document_files (in "..")
     "prepare_document"
     "pdfsetup.sty"
@@ -345,7 +348,7 @@
     "root.tex"
 
 session Prog_Prove (doc) in "Prog_Prove" = HOL +
-  options [document_logo = "HOL", document_build = "build",
+  options [document_logo = "HOL", document_bibliography, document_build = "build",
     document_variants = "prog-prove", show_question_marks = false]
   theories
     Basics
@@ -369,7 +372,8 @@
     "svmono.cls"
 
 session Sledgehammer (doc) in "Sledgehammer" = Pure +
-  options [document_logo = "S/H", document_build = "build", document_variants = "sledgehammer"]
+  options [document_logo = "S/H", document_bibliography, document_build = "build",
+    document_variants = "sledgehammer"]
   document_files (in "..")
     "prepare_document"
     "pdfsetup.sty"
@@ -380,7 +384,7 @@
     "root.tex"
 
 session System (doc) in "System" = Pure +
-  options [document_logo = "_", document_build = "build",
+  options [document_logo = "_", document_bibliography, document_build = "build",
     document_variants = "system", thy_output_source]
   sessions
     "HOL-Library"
@@ -408,7 +412,7 @@
     "root.tex"
 
 session Tutorial (doc) in "Tutorial" = HOL +
-  options [document_logo = "HOL", document_build = "build",
+  options [document_logo = "HOL", document_bibliography, document_build = "build",
     document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
   directories "Advanced" "CTL" "CodeGen" "Datatype" "Documents" "Fun" "Ifexpr"
     "Inductive" "Misc" "Protocol" "Rules" "Sets" "ToyList" "Trie" "Types"
@@ -502,7 +506,7 @@
     "types0.tex"
 
 session Typeclass_Hierarchy (doc) in "Typeclass_Hierarchy" = HOL +
-  options [document_logo = "Isar", document_build = "build",
+  options [document_logo = "Isar", document_bibliography, document_build = "build",
     document_variants = "typeclass_hierarchy"]
   sessions
     "HOL-Library"