diff -r 45137257399a -r 9bfb6978eb80 src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Jul 24 20:41:50 2012 +0200
+++ b/src/HOL/ROOT	Tue Jul 24 20:42:34 2012 +0200
@@ -114,6 +114,7 @@
     Author:     David von Oheimb
     Copyright   1999 TUM
   *}
+  options [document = false]
   theories EvenOdd
 
 session Import = HOL +
@@ -122,6 +123,7 @@
   theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
 
 session Number_Theory = HOL +
+  options [document = false]
   theories Number_Theory
 
 session Old_Number_Theory = HOL +
@@ -160,6 +162,7 @@
 
     Testing Metis and Sledgehammer.
   *}
+  options [document = false]
   theories
     Abstraction
     Big_O
@@ -176,6 +179,7 @@
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2009
   *}
+  options [document = false]
   theories [quick_and_dirty] Nitpick_Examples
 
 session Algebra = HOL +
@@ -286,10 +290,11 @@
   files "document/root.bib" "document/root.tex"
 
 session Decision_Procs = HOL +
+  options [document = false]
   theories Decision_Procs
 
 session ex in "Proofs/ex" = "HOL-Proofs" +
-  options [proofs = 2, parallel_proofs = 0]
+  options [document = false, proofs = 2, parallel_proofs = 0]
   theories Hilbert_Classical
 
 session Extraction in "Proofs/Extraction" = "HOL-Proofs" +
@@ -324,6 +329,7 @@
   description {*
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
   *}
+  options [document = false]
   theories Test Type
 
 session MicroJava = HOL +
@@ -375,6 +381,7 @@
     year=1995}
     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
   *}
+  options [document = false]
   theories Solve
 
 session Lattice = HOL +
@@ -509,15 +516,19 @@
 
 session TLA! = HOL +
   description {* The Temporal Logic of Actions *}
+  options [document = false]
   theories TLA
 
 session Inc in "TLA/Inc" = TLA +
+  options [document = false]
   theories Inc
 
 session Buffer in "TLA/Buffer" = TLA +
+  options [document = false]
   theories DBuffer
 
 session Memory in "TLA/Memory" = TLA +
+  options [document = false]
   theories MemoryImplementation
 
 session TPTP = HOL +
@@ -528,6 +539,7 @@
 
     TPTP-related extensions.
   *}
+  options [document = false]
   theories
     ATP_Theory_Export
     MaSh_Eval
@@ -559,9 +571,11 @@
   files "document/root.tex"
 
 session Nominal = HOL +
+  options [document = false]
   theories Nominal
 
 session Examples in "Nominal/Examples" = "HOL-Nominal" +
+  options [document = false]
   theories Nominal_Examples
   theories [quick_and_dirty] VC_Condition
 
@@ -571,6 +585,7 @@
   files "document/root.bib" "document/root.tex"
 
 session Examples in "Word/Examples" = "HOL-Word" +
+  options [document = false]
   theories WordExamples
 
 session Statespace = HOL +
@@ -583,16 +598,18 @@
   files "document/root.tex"
 
 session Examples in "NSA/Examples" = "HOL-NSA" +
+  options [document = false]
   theories NSPrimes
 
 session Mirabelle = HOL +
+  options [document = false]
   theories Mirabelle_Test
 (* FIXME
 	@cd Library; $(ISABELLE_TOOL) mirabelle -q arith Inner_Product.thy # some arbitrary small test case
 *)
 
 session SMT_Examples = "HOL-Word" +
-  options [quick_and_dirty]
+  options [document = false, quick_and_dirty]
   theories
     SMT_Tests
     SMT_Examples
@@ -602,10 +619,12 @@
     "SMT_Tests.certs"
 
 session "HOL-Boogie"! in "Boogie" = "HOL-Word" +
+  options [document = false]
   theories Boogie
   (* FIXME files!?! *)
 
 session Examples in "Boogie/Examples" = "HOL-Boogie" +
+  options [document = false]
   theories
     Boogie_Max_Stepwise
     Boogie_Max
@@ -617,9 +636,11 @@
     "VCC_Max.certs"
 
 session "HOL-SPARK"! in "SPARK" = "HOL-Word" +
+  options [document = false]
   theories SPARK
 
 session Examples in "SPARK/Examples" = "HOL-SPARK" +
+  options [document = false]
   theories
     "Gcd/Greatest_Common_Divisor"
 
@@ -705,15 +726,18 @@
     "simple_greatest_common_divisor/g_c_d.siv"
 
 session Mutabelle = HOL +
+  options [document = false]
   theories MutabelleExtra
 
 session Quickcheck_Examples = HOL +
+  options [document = false]
   theories Quickcheck_Examples  (* FIXME *)
 
 session Quotient_Examples = HOL +
   description {*
     Author:     Cezary Kaliszyk and Christian Urban
   *}
+  options [document = false]
   theories
     DList
     FSet
@@ -727,6 +751,7 @@
     Lift_DList
 
 session Predicate_Compile_Examples = HOL +
+  options [document = false]
   theories  (* FIXME *)
     Examples
     Predicate_Compile_Tests
@@ -757,14 +782,17 @@
   files "document/root.tex"
 
 session Library in "HOLCF/Library" = HOLCF +
+  options [document = false]
   theories HOLCF_Library
 
 session IMP in "HOLCF/IMP" = HOLCF +
+  options [document = false]
   theories HoareEx
   files "document/root.tex"
 
 session ex in "HOLCF/ex" = HOLCF +
   description {* Misc HOLCF examples *}
+  options [document = false]
   theories
     Dnat
     Dagstuhl
@@ -779,6 +807,7 @@
     Pattern_Match
 
 session FOCUS in "HOLCF/FOCUS" = HOLCF +
+  options [document = false]
   theories
     Fstreams
     FOCUS
@@ -790,6 +819,7 @@
 
     Formalization of a semantic model of I/O-Automata.
   *}
+  options [document = false]
   theories "meta_theory/Abstraction"
 
 session ABP in "HOLCF/IOA/ABP" = IOA +
@@ -798,6 +828,7 @@
 
     The Alternating Bit Protocol performed in I/O-Automata.
   *}
+  options [document = false]
   theories Correctness
 
 session NTP in "HOLCF/IOA/NTP" = IOA +
@@ -807,6 +838,7 @@
     A network transmission protocol, performed in the
     I/O automata formalization by Olaf Mueller.
   *}
+  options [document = false]
   theories Correctness
 
 session Storage in "HOLCF/IOA/Storage" = IOA +
@@ -815,18 +847,21 @@
 
     Memory storage case study.
   *}
+  options [document = false]
   theories Correctness
 
 session ex in "HOLCF/IOA/ex" = IOA +
   description {*
     Author:     Olaf Mueller
   *}
+  options [document = false]
   theories
     TrivEx
     TrivEx2
 
 session Datatype_Benchmark = HOL +
   description {* Some rather large datatype examples (from John Harrison). *}
+  options [document = false]
   theories [condition = ISABELLE_BENCHMARK]
     (* FIXME Toplevel.timing := true; *)
     Brackin
@@ -836,8 +871,8 @@
 
 session Record_Benchmark = HOL +
   description {* Some benchmark on large record. *}
+  options [document = false]
   theories [condition = ISABELLE_BENCHMARK]
     (* FIXME Toplevel.timing := true; *)
     Record_Benchmark
 
-