src/HOL/ROOT

 
 session "HOL-ex" in ex = HOL +
   description {*
     Miscellaneous examples for Higher-Order Logic.
   *}
+  options [document = false]
   sessions
     "HOL-Library"
     "HOL-Number_Theory"
-  theories [document = false]
-    "~~/src/HOL/Library/State_Monad"
+  theories
     Code_Binary_Nat_examples
-    "~~/src/HOL/Library/FuncSet"
     Eval_Examples
     Normalization_by_Evaluation
     Hebrew
     Chinese
     Serbian
-    "~~/src/HOL/Library/Refute"
-    "~~/src/HOL/Library/Transitive_Closure_Table"
     Cartouche_Examples
     Computations
-  theories
     Commands
     Adhoc_Overloading_Examples
     Iff_Oracle
     Coercion_Examples
     Peano_Axioms

     Argo_Examples
     Word_Type
     veriT_Preprocessing
   theories [skip_proofs = false]
     Meson_Test
-  document_files "root.bib" "root.tex"
 
 session "HOL-Isar_Examples" in Isar_Examples = HOL +
   description {*
     Miscellaneous Isabelle/Isar examples.
   *}