src/Doc/ROOT
changeset 65573 0f3fdf689bf9
parent 65569 3cb6f3281ef1
child 66444 6d2d993fa76e
--- a/src/Doc/ROOT	Mon Apr 24 11:23:07 2017 +0200
+++ b/src/Doc/ROOT	Mon Apr 24 11:52:51 2017 +0200
@@ -46,6 +46,8 @@
 
 session Corec (doc) in "Corec" = "HOL-Library" +
   options [document_variants = "corec"]
+  sessions
+    Datatypes
   theories [document = false] "../Datatypes/Setup"
   theories Corec
   document_files (in "..")
@@ -170,7 +172,7 @@
     "root.tex"
     "style.sty"
 
-session Isar_Ref (doc) in "Isar_Ref" = HOL +
+session Isar_Ref (doc) in "Isar_Ref" = "HOL-Library" +
   options [document_variants = "isar-ref", quick_and_dirty, thy_output_source]
   theories
     Preface
@@ -244,7 +246,9 @@
 
 session Sugar (doc) in "Sugar" = HOL +
   options [document_variants = "sugar"]
-  theories [document = ""]
+  sessions
+    "HOL-Library"
+  theories [document = false]
     "~~/src/HOL/Library/LaTeXsugar"
     "~~/src/HOL/Library/OptionalSugar"
   theories Sugar
@@ -436,7 +440,7 @@
   theories
     "Protocol/NS_Public"
     "Documents/Documents"
-  theories [document = ""]
+  theories [document = false]
     "Types/Setup"
   theories [thy_output_margin = 64, thy_output_indent = 0]
     "Types/Numbers"
@@ -502,7 +506,7 @@
     "root.tex"
     "style.sty"
 
-session Typeclass_Hierarchy_Basics in "Typeclass_Hierarchy" = "HOL" +
+session Typeclass_Hierarchy_Basics in "Typeclass_Hierarchy" = "HOL-Library" +
   options [document = false]
   theories
     Setup