src/HOL/ROOT
changeset 65548 b7caa2b8bdbf
parent 65544 c09c11386ca5
child 65549 263f2a046308
--- a/src/HOL/ROOT	Fri Apr 21 21:06:02 2017 +0200
+++ b/src/HOL/ROOT	Fri Apr 21 21:36:49 2017 +0200
@@ -577,23 +577,19 @@
   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
@@ -669,7 +665,6 @@
     veriT_Preprocessing
   theories [skip_proofs = false]
     Meson_Test
-  document_files "root.bib" "root.tex"
 
 session "HOL-Isar_Examples" in Isar_Examples = HOL +
   description {*