diff -r e59778bc71a0 -r fd03877ad5bc doc-src/ROOT
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/ROOT	Wed Jul 25 18:05:07 2012 +0200
@@ -0,0 +1,116 @@
+session Classes! in "Classes/Thy" = HOL +
+  options [browser_info = false, document = false, document_dump = document, document_dump_only]
+  theories [document = false] Setup
+  theories Classes
+
+session Codegen! in "Codegen/Thy" = "HOL-Library" +
+  options [browser_info = false, document = false, document_dump = document, document_dump_only,
+    print_mode = "no_brackets,iff"]
+  theories [document = false] Setup
+  theories
+    Introduction
+    Foundations
+    Refinement
+    Inductive_Predicate
+    Evaluation
+    Adaptation
+    Further
+
+session Functions! in "Functions/Thy" = HOL +
+  options [browser_info = false, document = false, document_dump = document, document_dump_only]
+  theories Functions
+
+session IsarImplementation! in "IsarImplementation/Thy" = HOL +
+  options [browser_info = false, document = false, document_dump = document, document_dump_only]
+  theories
+    Eq
+    Integration
+    Isar
+    Local_Theory
+    Logic
+    ML
+    Prelim
+    Proof
+    Syntax
+    Tactic
+
+session IsarRef in "IsarRef/Thy" = HOL +
+  options [browser_info = false, document = false, document_dump = document, document_dump_only,
+    quick_and_dirty]
+  theories
+    Preface
+    Synopsis
+    Framework
+    First_Order_Logic
+    Outer_Syntax
+    Document_Preparation
+    Spec
+    Proof
+    Inner_Syntax
+    Misc
+    Generic
+    HOL_Specific
+    Quick_Reference
+    Symbols
+    ML_Tactic
+
+session IsarRef in "IsarRef/Thy" = HOLCF +
+  options [browser_info = false, document = false, document_dump = document, document_dump_only,
+    quick_and_dirty]
+  theories HOLCF_Specific
+
+session IsarRef in "IsarRef/Thy" = ZF +
+  options [browser_info = false, document = false, document_dump = document, document_dump_only,
+    quick_and_dirty]
+  theories ZF_Specific
+
+session LaTeXsugar! in "LaTeXsugar/Sugar" = HOL +
+  options [browser_info = false, document = false, document_dump = document, document_dump_only,
+    threads = 1]  (* FIXME *)
+  theories [document_dump = ""]
+    "~~/src/HOL/Library/LaTeXsugar"
+    "~~/src/HOL/Library/OptionalSugar"
+  theories Sugar
+
+session Locales! in "Locales/Locales" = HOL +
+  options [browser_info = false, document = false, document_dump = document, document_dump_only]
+  theories
+    Examples1
+    Examples2
+    Examples3
+
+session Main! in "Main/Docs" = HOL +
+  options [browser_info = false, document = false, document_dump = document, document_dump_only]
+  theories Main_Doc
+
+session ProgProve! in "ProgProve/Thys" = HOL +
+  options [browser_info = false, document = false, document_dump = document, document_dump_only,
+    show_question_marks = false]
+  theories
+    Basics
+    Bool_nat_list
+    MyList
+    Types_and_funs
+    Logic
+    Isar
+
+session System! in "System/Thy" = Pure +
+  options [browser_info = false, document = false, document_dump = document, document_dump_only]
+  theories
+    Basics
+    Interfaces
+    Scala
+    Presentation
+    Misc
+
+(* session Tutorial in "Tutorial" = HOL + FIXME *)
+
+session examples in "ZF" = ZF +
+  options [browser_info = false, document = false, document_dump = document, document_dump_only,
+    print_mode = "brackets"]
+  theories
+    IFOL_examples
+    FOL_examples
+    ZF_examples
+    If
+