src/HOL/ROOT

 
 session "HOL-Proofs" (timing) = Pure +
   description {*
     HOL-Main with explicit proof terms.
   *}
-  options [document = false, quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
+  options [quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
   sessions
     "HOL-Library"
   theories
     "HOL-Library.Old_Datatype"
 

 
     This is an extension of IMP with local variables and mutually recursive
     procedures. For documentation see "Hoare Logic for Mutual Recursion and
     Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
   *}
-  options [document = false]
   theories EvenOdd
 
 session "HOL-Data_Structures" (timing) in Data_Structures = HOL +
   options [document_variants = document]
   sessions

   *}
   theories Hoare_Parallel
   document_files "root.bib" "root.tex"
 
 session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Number_Theory" +
-  options [document = false, browser_info = false]
+  options [browser_info = false]
   sessions
     "HOL-Data_Structures"
     "HOL-ex"
   theories
     Generate

     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Jasmin Blanchette, TU Muenchen
 
     Testing Metis and Sledgehammer.
   *}
-  options [document = false]
   sessions
     "HOL-Decision_Procs"
   theories
     Abstraction
     Big_O

 session "HOL-Nitpick_Examples" in Nitpick_Examples = "HOL-Library" +
   description {*
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2009
   *}
-  options [document = false]
   theories [quick_and_dirty] Nitpick_Examples
 
 session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" +
   description {*
     Author: Clemens Ballarin, started 24 September 1999

 
 session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" +
   description {*
     Various decision procedures, typically involving reflection.
   *}
-  options [document = false]
   theories
     Decision_Procs
 
 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
-  options [document = false]
   sessions
     "HOL-Isar_Examples"
   theories
     Hilbert_Classical
     Proof_Terms

 
     This is a simple exploratory implementation of Lambda-Prolog in HOL,
     including some minimal examples (in Test.thy) and a more typical example of
     a little functional language and its type system.
   *}
-  options [document = false]
   theories Test Type
 
 session "HOL-MicroJava" (timing) in MicroJava = "HOL-Library" +
   description {*
     Formalization of a fragment of Java, together with a corresponding virtual

     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 "HOL-Lattice" in Lattice = HOL +
   description {*
     Author:     Markus Wenzel, TU Muenchen

 
 session "HOL-ex" (timing) in ex = "HOL-Number_Theory" +
   description {*
     Miscellaneous examples for Higher-Order Logic.
   *}
-  options [document = false]
   theories
     Adhoc_Overloading_Examples
     Antiquote
     Argo_Examples
     Arith_Examples

 
 session "HOL-TLA" in TLA = HOL +
   description {*
     Lamport's Temporal Logic of Actions.
   *}
-  options [document = false]
   theories TLA
 
 session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
-  options [document = false]
   theories Inc
 
 session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
-  options [document = false]
   theories DBuffer
 
 session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
-  options [document = false]
   theories MemoryImplementation
 
 session "HOL-TPTP" in TPTP = "HOL-Library" +
   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
     TPTP_Interpret
     THF_Arith

     Dining_Cryptographers
     Koepf_Duermuth_Countermeasure
     Measure_Not_CCC
 
 session "HOL-Nominal" in Nominal = "HOL-Library" +
-  options [document = false]
   theories
     Nominal
 
 session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" +
-  options [document = false]
   theories
     Class3
     CK_Machine
     Compile
     Contexts

 
 session "HOL-Datatype_Examples" (timing) in Datatype_Examples = "HOL-Library" +
   description {*
     (Co)datatype Examples.
   *}
-  options [document = false]
   theories
     Compat
     Lambda_Term
     Process
     TreeFsetI

 
 session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" +
   description {*
     Corecursion Examples.
   *}
-  options [document = false]
   theories
     LFilter
     Paper_Examples
     Stream_Processor
     "Tests/Simple_Nesting"

     WordBitwise
     Bit_Comparison
   document_files "root.bib" "root.tex"
 
 session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
-  options [document = false]
   theories WordExamples
 
 session "HOL-Statespace" in Statespace = HOL +
   theories [skip_proofs = false]
     StateSpaceEx

   theories
     Nonstandard_Analysis
   document_files "root.tex"
 
 session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" +
-  options [document = false]
   theories
     NSPrimes
 
 session "HOL-Mirabelle" in Mirabelle = HOL +
-  options [document = false]
   theories Mirabelle_Test
 
 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
-  options [document = false, timeout = 60]
+  options [timeout = 60]
   theories Ex
 
 session "HOL-Word-SMT_Examples" (timing) in SMT_Examples = "HOL-Word" +
-  options [document = false, quick_and_dirty]
+  options [quick_and_dirty]
   theories
     Boogie
     SMT_Examples
     SMT_Word_Examples
     SMT_Tests
 
 session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
-  options [document = false]
   theories
     SPARK (global)
 
 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
-  options [document = false, spark_prv = false]
+  options [spark_prv = false]
   theories
     "Gcd/Greatest_Common_Divisor"
     "Liseq/Longest_Increasing_Subsequence"
     "RIPEMD-160/F"
     "RIPEMD-160/Hash"

     "root.tex"
     "Simple_Gcd.adb"
     "Simple_Gcd.ads"
 
 session "HOL-Mutabelle" in Mutabelle = "HOL-Library" +
-  options [document = false]
   theories MutabelleExtra
 
 session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = "HOL-Library" +
-  options [document = false]
   theories
     Quickcheck_Examples
     Quickcheck_Lattice_Examples
     Completeness
     Quickcheck_Interfaces

 
 session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Algebra" +
   description {*
     Author:     Cezary Kaliszyk and Christian Urban
   *}
-  options [document = false]
   theories
     DList
     Quotient_FSet
     Quotient_Int
     Quotient_Message

     Lift_DList
     Int_Pow
     Lifting_Code_Dt_Test
 
 session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = "HOL-Library" +
-  options [document = false]
   theories
     Examples
     Predicate_Compile_Tests
     Predicate_Compile_Quickcheck_Examples
     Specialisation_Examples

 
 session "HOL-Types_To_Sets" in Types_To_Sets = HOL +
   description {*
     Experimental extension of Higher-Order Logic to allow translation of types to sets.
   *}
-  options [document = false]
   theories
     Types_To_Sets
     "Examples/Prerequisites"
     "Examples/Finite"
     "Examples/T2_Spaces"

     Fixrec_ex
     New_Domain
   document_files "root.tex"
 
 session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
-  options [document = false]
   theories
     HOLCF_Library
     HOL_Cpo
 
 session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
   description {*
     IMP -- A WHILE-language and its Semantics.
 
     This is the HOLCF-based denotational semantics of a simple WHILE-language.
   *}
-  options [document = false]
   sessions
     "HOL-IMP"
   theories
     HoareEx
   document_files "root.tex"
 
 session "HOLCF-ex" in "HOLCF/ex" = "HOLCF-Library" +
   description {*
     Miscellaneous examples for HOLCF.
   *}
-  options [document = false]
   theories
     Dnat
     Dagstuhl
     Focus_ex
     Fix2

     http://www4.in.tum.de/publ/html.php?e=15
 
     "Specification and Development of Interactive Systems: Focus on Streams,
     Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
   *}
-  options [document = false]
   theories
     Fstreams
     FOCUS
     Buffer_adm
 

 
     The distribution contains simulation relations, temporal logic, and an
     abstraction theory. Everything is based upon a domain-theoretic model of
     finite and infinite sequences.
   *}
-  options [document = false]
   theories Abstraction
 
 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
   description {*
     Author:     Olaf Mueller
 
     The Alternating Bit Protocol performed in I/O-Automata.
   *}
-  options [document = false]
   theories
     Correctness
     Spec
 
 session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +

     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 "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
   description {*
     Author:     Olaf Mueller
 
     Memory storage case study.
   *}
-  options [document = false]
   theories Correctness
 
 session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
   description {*
     Author:     Olaf Mueller
   *}
-  options [document = false]
   theories
     TrivEx
     TrivEx2