1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/ROOT	Wed Jul 25 18:05:07 2012 +0200
     1.3 @@ -0,0 +1,116 @@
     1.4 +session Classes! in "Classes/Thy" = HOL +
     1.5 +  options [browser_info = false, document = false, document_dump = document, document_dump_only]
     1.6 +  theories [document = false] Setup
     1.7 +  theories Classes
     1.8 +
     1.9 +session Codegen! in "Codegen/Thy" = "HOL-Library" +
    1.10 +  options [browser_info = false, document = false, document_dump = document, document_dump_only,
    1.11 +    print_mode = "no_brackets,iff"]
    1.12 +  theories [document = false] Setup
    1.13 +  theories
    1.14 +    Introduction
    1.15 +    Foundations
    1.16 +    Refinement
    1.17 +    Inductive_Predicate
    1.18 +    Evaluation
    1.19 +    Adaptation
    1.20 +    Further
    1.21 +
    1.22 +session Functions! in "Functions/Thy" = HOL +
    1.23 +  options [browser_info = false, document = false, document_dump = document, document_dump_only]
    1.24 +  theories Functions
    1.25 +
    1.26 +session IsarImplementation! in "IsarImplementation/Thy" = HOL +
    1.27 +  options [browser_info = false, document = false, document_dump = document, document_dump_only]
    1.28 +  theories
    1.29 +    Eq
    1.30 +    Integration
    1.31 +    Isar
    1.32 +    Local_Theory
    1.33 +    Logic
    1.34 +    ML
    1.35 +    Prelim
    1.36 +    Proof
    1.37 +    Syntax
    1.38 +    Tactic
    1.39 +
    1.40 +session IsarRef in "IsarRef/Thy" = HOL +
    1.41 +  options [browser_info = false, document = false, document_dump = document, document_dump_only,
    1.42 +    quick_and_dirty]
    1.43 +  theories
    1.44 +    Preface
    1.45 +    Synopsis
    1.46 +    Framework
    1.47 +    First_Order_Logic
    1.48 +    Outer_Syntax
    1.49 +    Document_Preparation
    1.50 +    Spec
    1.51 +    Proof
    1.52 +    Inner_Syntax
    1.53 +    Misc
    1.54 +    Generic
    1.55 +    HOL_Specific
    1.56 +    Quick_Reference
    1.57 +    Symbols
    1.58 +    ML_Tactic
    1.59 +
    1.60 +session IsarRef in "IsarRef/Thy" = HOLCF +
    1.61 +  options [browser_info = false, document = false, document_dump = document, document_dump_only,
    1.62 +    quick_and_dirty]
    1.63 +  theories HOLCF_Specific
    1.64 +
    1.65 +session IsarRef in "IsarRef/Thy" = ZF +
    1.66 +  options [browser_info = false, document = false, document_dump = document, document_dump_only,
    1.67 +    quick_and_dirty]
    1.68 +  theories ZF_Specific
    1.69 +
    1.70 +session LaTeXsugar! in "LaTeXsugar/Sugar" = HOL +
    1.71 +  options [browser_info = false, document = false, document_dump = document, document_dump_only,
    1.72 +    threads = 1]  (* FIXME *)
    1.73 +  theories [document_dump = ""]
    1.74 +    "~~/src/HOL/Library/LaTeXsugar"
    1.75 +    "~~/src/HOL/Library/OptionalSugar"
    1.76 +  theories Sugar
    1.77 +
    1.78 +session Locales! in "Locales/Locales" = HOL +
    1.79 +  options [browser_info = false, document = false, document_dump = document, document_dump_only]
    1.80 +  theories
    1.81 +    Examples1
    1.82 +    Examples2
    1.83 +    Examples3
    1.84 +
    1.85 +session Main! in "Main/Docs" = HOL +
    1.86 +  options [browser_info = false, document = false, document_dump = document, document_dump_only]
    1.87 +  theories Main_Doc
    1.88 +
    1.89 +session ProgProve! in "ProgProve/Thys" = HOL +
    1.90 +  options [browser_info = false, document = false, document_dump = document, document_dump_only,
    1.91 +    show_question_marks = false]
    1.92 +  theories
    1.93 +    Basics
    1.94 +    Bool_nat_list
    1.95 +    MyList
    1.96 +    Types_and_funs
    1.97 +    Logic
    1.98 +    Isar
    1.99 +
   1.100 +session System! in "System/Thy" = Pure +
   1.101 +  options [browser_info = false, document = false, document_dump = document, document_dump_only]
   1.102 +  theories
   1.103 +    Basics
   1.104 +    Interfaces
   1.105 +    Scala
   1.106 +    Presentation
   1.107 +    Misc
   1.108 +
   1.109 +(* session Tutorial in "Tutorial" = HOL + FIXME *)
   1.110 +
   1.111 +session examples in "ZF" = ZF +
   1.112 +  options [browser_info = false, document = false, document_dump = document, document_dump_only,
   1.113 +    print_mode = "brackets"]
   1.114 +  theories
   1.115 +    IFOL_examples
   1.116 +    FOL_examples
   1.117 +    ZF_examples
   1.118 +    If
   1.119 +