doc-src/ROOT

more standard document preparation within session context;

session Classes (doc) in "Classes/Thy" = HOL +
  options [browser_info = false, document = false,
    document_dump = document, document_dump_mode = "tex"]
  theories [document = false] Setup
  theories Classes

session Codegen (doc) in "Codegen/Thy" = "HOL-Library" +
  options [browser_info = false, document = false,
    document_dump = document, document_dump_mode = "tex",
    print_mode = "no_brackets,iff"]
  theories [document = false] Setup
  theories
    Introduction
    Foundations
    Refinement
    Inductive_Predicate
    Evaluation
    Adaptation
    Further

session Functions (doc) in "Functions/Thy" = HOL +
  options [browser_info = false, document = false,
    document_dump = document, document_dump_mode = "tex"]
  theories Functions

session IsarImplementation (doc) in "IsarImplementation" = HOL +
  options [document_variants = "implementation"]
  theories
    Eq
    Integration
    Isar
    Local_Theory
    Logic
    ML
    Prelim
    Proof
    Syntax
    Tactic
  files
    "../iman.sty"
    "../extra.sty"
    "../isar.sty"
    "../proof.sty"
    "../underscore.sty"
    "../ttbox.sty"
    "../manual.bib"
    "document/build"
    "document/root.tex"
    "document/style.sty"

session "HOL-IsarRef" (doc) in "IsarRef/Thy" = HOL +
  options [browser_info = false, document = false,
    document_dump = document, document_dump_mode = "tex",
    quick_and_dirty]
  theories
    Preface
    Synopsis
    Framework
    First_Order_Logic
    Outer_Syntax
    Document_Preparation
    Spec
    Proof
    Inner_Syntax
    Misc
    Generic
    HOL_Specific
    Quick_Reference
    Symbols
    ML_Tactic

session "HOLCF-IsarRef" (doc) in "IsarRef/Thy" = HOLCF +
  options [browser_info = false, document = false,
    document_dump = document, document_dump_mode = "tex",
    quick_and_dirty]
  theories HOLCF_Specific

session "ZF-IsarRef" (doc) in "IsarRef/Thy" = ZF +
  options [browser_info = false, document = false,
    document_dump = document, document_dump_mode = "tex",
    quick_and_dirty]
  theories ZF_Specific

session LaTeXsugar (doc) in "LaTeXsugar/Sugar" = HOL +
  options [browser_info = false, document = false,
    document_dump = document, document_dump_mode = "tex"]
  theories [document_dump = ""]
    "~~/src/HOL/Library/LaTeXsugar"
    "~~/src/HOL/Library/OptionalSugar"
  theories Sugar

session Locales (doc) in "Locales/Locales" = HOL +
  options [browser_info = false, document = false,
    document_dump = document, document_dump_mode = "tex"]
  theories
    Examples1
    Examples2
    Examples3

session Main (doc) in "Main/Docs" = HOL +
  options [browser_info = false, document = false,
    document_dump = document, document_dump_mode = "tex"]
  theories Main_Doc

session ProgProve (doc) in "ProgProve/Thys" = HOL +
  options [browser_info = false, document = false,
    document_dump = document, document_dump_mode = "tex",
    show_question_marks = false]
  theories
    Basics
    Bool_nat_list
    MyList
    Types_and_funs
    Logic
    Isar

session Ref (doc) in "Ref" = Pure +
  options [document_variants = "ref"]
  theories
  files
    "../iman.sty"
    "../extra.sty"
    "../ttbox.sty"
    "../proof.sty"
    "../manual.bib"
    "document/build"
    "document/classical.tex"
    "document/root.tex"
    "document/simplifier.tex"
    "document/substitution.tex"
    "document/syntax.tex"
    "document/tactic.tex"
    "document/thm.tex"

session System (doc) in "System" = Pure +
  options [document_variants = "system", thy_output_source]
  theories
    Basics
    Interfaces
    Sessions
    Presentation
    Scala
    Misc
  files
    "../IsarRef/style.sty"
    "../iman.sty"
    "../extra.sty"
    "../ttbox.sty"
    "../isar.sty"
    "../underscore.sty"
    "../manual.bib"
    "document/browser_screenshot.eps"
    "document/browser_screenshot.png"
    "document/build"
    "document/root.tex"

session Tutorial (doc) in "TutorialI" = HOL +
  options [browser_info = false, document = false,
    document_dump = document, document_dump_mode = "tex",
    print_mode = "brackets"]
  theories [thy_output_indent = 5]
    "ToyList/ToyList"
    "Ifexpr/Ifexpr"
    "CodeGen/CodeGen"
    "Trie/Trie"
    "Datatype/ABexpr"
    "Datatype/unfoldnested"
    "Datatype/Nested"
    "Datatype/Fundata"
    "Fun/fun0"
    "Advanced/simp2"
    "CTL/PDL"
    "CTL/CTL"
    "CTL/CTLind"
    "Inductive/Even"
    "Inductive/Mutual"
    "Inductive/Star"
    "Inductive/AB"
    "Inductive/Advanced"
    "Misc/Tree"
    "Misc/Tree2"
    "Misc/Plus"
    "Misc/case_exprs"
    "Misc/fakenat"
    "Misc/natsum"
    "Misc/pairs2"
    "Misc/Option2"
    "Misc/types"
    "Misc/prime_def"
    "Misc/simp"
    "Misc/Itrev"
    "Misc/AdvancedInd"
    "Misc/appendix"
  theories
    "Protocol/NS_Public"
    "Documents/Documents"
  theories [document_dump = ""]
    "Types/Setup"
  theories [pretty_margin = 64, thy_output_indent = 0]
    "Types/Numbers"
    "Types/Pairs"
    "Types/Records"
    "Types/Typedefs"
    "Types/Overloading"
    "Types/Axioms"
    "Rules/Basic"
    "Rules/Blast"
    "Rules/Force"
  theories [pretty_margin = 64, thy_output_indent = 5]
    "Rules/Primes"
    "Rules/Forward"
    "Rules/Tacticals"
    "Rules/find2"
    "Sets/Examples"
    "Sets/Functions"
    "Sets/Relations"
    "Sets/Recur"

session "HOL-ToyList2" (doc) in "TutorialI/ToyList2" = HOL +
  options [browser_info = false, document = false, print_mode = "brackets"]
  theories ToyList

session "ZF-examples" (doc) in "ZF" = ZF +
  options [browser_info = false, document = false,
    document_dump = document, document_dump_mode = "tex",
    print_mode = "brackets"]
  theories
    IFOL_examples
    FOL_examples
    ZF_examples
    If