src/HOL/ROOT

 session IMPP = HOL +
   description {*
     Author:     David von Oheimb
     Copyright   1999 TUM
   *}
+  options [document = false]
   theories EvenOdd
 
 session Import = HOL +
   options [document_graph]
   theories HOL_Light_Maps
   theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
 
 session Number_Theory = HOL +
+  options [document = false]
   theories Number_Theory
 
 session Old_Number_Theory = HOL +
   options [document_graph]
   theories [document = false]

     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Jasmin Blanchette, TU Muenchen
 
     Testing Metis and Sledgehammer.
   *}
+  options [document = false]
   theories
     Abstraction
     Big_O
     Binary_Tree
     Clausification

 session Nitpick_Examples = HOL +
   description {*
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2009
   *}
+  options [document = false]
   theories [quick_and_dirty] Nitpick_Examples
 
 session Algebra = HOL +
   description {*
     Author: Clemens Ballarin, started 24 September 1999

     "~~/src/HOL/Library/LaTeXsugar"
   theories Imperative_HOL_ex
   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" +
   description {* Examples for program extraction in Higher-Order Logic *}
   options [proofs = 2, parallel_proofs = 0]

 
 session Prolog = HOL +
   description {*
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
   *}
+  options [document = false]
   theories Test Type
 
 session MicroJava = HOL +
   options [document_graph]
   theories [document = false] "~~/src/HOL/Library/While_Combinator"

     booktitle={Proc.\ TACAS Workshop},
     organization={Aarhus University, BRICS report},
     year=1995}
     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
   *}
+  options [document = false]
   theories Solve
 
 session Lattice = HOL +
   description {*
     Author:     Markus Wenzel, TU Muenchen

   theories Cplex
   files "document/root.tex"
 
 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 +
   description {*
     Author:     Jasmin Blanchette, TU Muenchen
     Author:     Nik Sultana, University of Cambridge
     Copyright   2011
 
     TPTP-related extensions.
   *}
+  options [document = false]
   theories
     ATP_Theory_Export
     MaSh_Eval
     MaSh_Export
     TPTP_Interpret

     "ex/Dining_Cryptographers"
     "ex/Koepf_Duermuth_Countermeasure"
   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
 
 session Word = HOL +
   options [document_graph]
   theories Word
   files "document/root.bib" "document/root.tex"
 
 session Examples in "Word/Examples" = "HOL-Word" +
+  options [document = false]
   theories WordExamples
 
 session Statespace = HOL +
   theories StateSpaceEx
   files "document/root.tex"

   options [document_graph]
   theories Hypercomplex
   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
     SMT_Word_Examples
   files
     "SMT_Examples.certs"
     "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
     Boogie_Dijkstra
     VCC_Max

     "Boogie_Dijkstra.certs"
     "Boogie_Max.certs"
     "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"
 
     "Liseq/Longest_Increasing_Subsequence"
 

     "simple_greatest_common_divisor/g_c_d.fdl"
     "simple_greatest_common_divisor/g_c_d.rls"
     "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
     Quotient_Int
     Quotient_Message

     Lift_Fun
     Quotient_Rat
     Lift_DList
 
 session Predicate_Compile_Examples = HOL +
+  options [document = false]
   theories  (* FIXME *)
     Examples
     Predicate_Compile_Tests
     Specialisation_Examples
 

     Fixrec_ex
     New_Domain
   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
     Focus_ex
     Fix2

     Domain_Proofs
     Letrec
     Pattern_Match
 
 session FOCUS in "HOLCF/FOCUS" = HOLCF +
+  options [document = false]
   theories
     Fstreams
     FOCUS
     Buffer_adm
 

   description {*
     Author:     Olaf Mueller
 
     Formalization of a semantic model of I/O-Automata.
   *}
+  options [document = false]
   theories "meta_theory/Abstraction"
 
 session ABP in "HOLCF/IOA/ABP" = IOA +
   description {*
     Author:     Olaf Mueller
 
     The Alternating Bit Protocol performed in I/O-Automata.
   *}
+  options [document = false]
   theories Correctness
 
 session NTP in "HOLCF/IOA/NTP" = IOA +
   description {*
     Author:     Tobias Nipkow & Konrad Slind
 
     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 +
   description {*
     Author:     Olaf Mueller
 
     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
     Instructions
     SML
     Verilog
 
 session Record_Benchmark = HOL +
   description {* Some benchmark on large record. *}
+  options [document = false]
   theories [condition = ISABELLE_BENCHMARK]
     (* FIXME Toplevel.timing := true; *)
     Record_Benchmark
 
-