src/Doc/ROOT
changeset 48985 5386df44a037
parent 48971 5a4bcf466156
child 49318 612a04e7c853
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Doc/ROOT	Tue Aug 28 18:57:32 2012 +0200
     1.3 @@ -0,0 +1,387 @@
     1.4 +session Classes (doc) in "Classes" = HOL +
     1.5 +  options [document_variants = "classes"]
     1.6 +  theories [document = false] Setup
     1.7 +  theories Classes
     1.8 +  files
     1.9 +    "../prepare_document"
    1.10 +    "../pdfsetup.sty"
    1.11 +    "document/build"
    1.12 +    "document/root.tex"
    1.13 +    "document/style.sty"
    1.14 +
    1.15 +session Codegen (doc) in "Codegen" = "HOL-Library" +
    1.16 +  options [document_variants = "codegen", print_mode = "no_brackets,iff"]
    1.17 +  theories [document = false] Setup
    1.18 +  theories
    1.19 +    Introduction
    1.20 +    Foundations
    1.21 +    Refinement
    1.22 +    Inductive_Predicate
    1.23 +    Evaluation
    1.24 +    Adaptation
    1.25 +    Further
    1.26 +  files
    1.27 +    "../prepare_document"
    1.28 +    "../pdfsetup.sty"
    1.29 +    "document/adapt.tex"
    1.30 +    "document/architecture.tex"
    1.31 +    "document/build"
    1.32 +    "document/root.tex"
    1.33 +    "document/style.sty"
    1.34 +
    1.35 +session Functions (doc) in "Functions" = HOL +
    1.36 +  options [document_variants = "functions"]
    1.37 +  theories Functions
    1.38 +  files
    1.39 +    "../prepare_document"
    1.40 +    "../pdfsetup.sty"
    1.41 +    "../iman.sty"
    1.42 +    "../extra.sty"
    1.43 +    "../isar.sty"
    1.44 +    "../manual.bib"
    1.45 +    "document/build"
    1.46 +    "document/conclusion.tex"
    1.47 +    "document/intro.tex"
    1.48 +    "document/mathpartir.sty"
    1.49 +    "document/root.tex"
    1.50 +    "document/style.sty"
    1.51 +
    1.52 +session Intro (doc) in "Intro" = Pure +
    1.53 +  options [document_variants = "intro"]
    1.54 +  theories
    1.55 +  files
    1.56 +    "../prepare_document"
    1.57 +    "../pdfsetup.sty"
    1.58 +    "../iman.sty"
    1.59 +    "../extra.sty"
    1.60 +    "../ttbox.sty"
    1.61 +    "../proof.sty"
    1.62 +    "../manual.bib"
    1.63 +    "document/build"
    1.64 +    "document/root.tex"
    1.65 +
    1.66 +session IsarImplementation (doc) in "IsarImplementation" = HOL +
    1.67 +  options [document_variants = "implementation"]
    1.68 +  theories
    1.69 +    Eq
    1.70 +    Integration
    1.71 +    Isar
    1.72 +    Local_Theory
    1.73 +    Logic
    1.74 +    ML
    1.75 +    Prelim
    1.76 +    Proof
    1.77 +    Syntax
    1.78 +    Tactic
    1.79 +  files
    1.80 +    "../prepare_document"
    1.81 +    "../pdfsetup.sty"
    1.82 +    "../iman.sty"
    1.83 +    "../extra.sty"
    1.84 +    "../isar.sty"
    1.85 +    "../proof.sty"
    1.86 +    "../underscore.sty"
    1.87 +    "../ttbox.sty"
    1.88 +    "../manual.bib"
    1.89 +    "document/build"
    1.90 +    "document/root.tex"
    1.91 +    "document/style.sty"
    1.92 +
    1.93 +session IsarRef (doc) in "IsarRef" = HOL +
    1.94 +  options [document_variants = "isar-ref", quick_and_dirty, thy_output_source]
    1.95 +  theories
    1.96 +    Preface
    1.97 +    Synopsis
    1.98 +    Framework
    1.99 +    First_Order_Logic
   1.100 +    Outer_Syntax
   1.101 +    Document_Preparation
   1.102 +    Spec
   1.103 +    Proof
   1.104 +    Inner_Syntax
   1.105 +    Misc
   1.106 +    Generic
   1.107 +    HOL_Specific
   1.108 +    Quick_Reference
   1.109 +    Symbols
   1.110 +    ML_Tactic
   1.111 +  files
   1.112 +    "../prepare_document"
   1.113 +    "../pdfsetup.sty"
   1.114 +    "../iman.sty"
   1.115 +    "../extra.sty"
   1.116 +    "../ttbox.sty"
   1.117 +    "../proof.sty"
   1.118 +    "../isar.sty"
   1.119 +    "../manual.bib"
   1.120 +    "document/build"
   1.121 +    "document/isar-vm.eps"
   1.122 +    "document/isar-vm.pdf"
   1.123 +    "document/isar-vm.svg"
   1.124 +    "document/root.tex"
   1.125 +    "document/showsymbols"
   1.126 +    "document/style.sty"
   1.127 +
   1.128 +session LaTeXsugar (doc) in "LaTeXsugar" = HOL +
   1.129 +  options [document_variants = "sugar"]
   1.130 +  theories [document = ""]
   1.131 +    "~~/src/HOL/Library/LaTeXsugar"
   1.132 +    "~~/src/HOL/Library/OptionalSugar"
   1.133 +  theories Sugar
   1.134 +  files
   1.135 +    "../prepare_document"
   1.136 +    "../pdfsetup.sty"
   1.137 +    "document/build"
   1.138 +    "document/mathpartir.sty"
   1.139 +    "document/root.bib"
   1.140 +    "document/root.tex"
   1.141 +
   1.142 +session Locales (doc) in "Locales" = HOL +
   1.143 +  options [document_variants = "locales", pretty_margin = 65]
   1.144 +  theories
   1.145 +    Examples1
   1.146 +    Examples2
   1.147 +    Examples3
   1.148 +  files
   1.149 +    "../prepare_document"
   1.150 +    "../pdfsetup.sty"
   1.151 +    "document/build"
   1.152 +    "document/root.tex"
   1.153 +
   1.154 +session Logics (doc) in "Logics" = Pure +
   1.155 +  options [document_variants = "logics"]
   1.156 +  theories
   1.157 +  files
   1.158 +    "../prepare_document"
   1.159 +    "../pdfsetup.sty"
   1.160 +    "../iman.sty"
   1.161 +    "../extra.sty"
   1.162 +    "../ttbox.sty"
   1.163 +    "../proof.sty"
   1.164 +    "../manual.bib"
   1.165 +    "document/build"
   1.166 +    "document/root.tex"
   1.167 +
   1.168 +session "Logics-HOL" (doc) in "HOL" = Pure +
   1.169 +  options [document_variants = "logics-HOL"]
   1.170 +  theories
   1.171 +  files
   1.172 +    "../prepare_document"
   1.173 +    "../pdfsetup.sty"
   1.174 +    "../iman.sty"
   1.175 +    "../extra.sty"
   1.176 +    "../ttbox.sty"
   1.177 +    "../proof.sty"
   1.178 +    "../manual.bib"
   1.179 +    "../Logics/document/syntax.tex"
   1.180 +    "document/build"
   1.181 +    "document/root.tex"
   1.182 +
   1.183 +session "Logics-ZF" (doc) in "ZF" = ZF +
   1.184 +  options [document_variants = "logics-ZF", print_mode = "brackets",
   1.185 +    thy_output_source]
   1.186 +  theories
   1.187 +    IFOL_examples
   1.188 +    FOL_examples
   1.189 +    ZF_examples
   1.190 +    If
   1.191 +    ZF_Isar
   1.192 +  files
   1.193 +    "../prepare_document"
   1.194 +    "../pdfsetup.sty"
   1.195 +    "../isar.sty"
   1.196 +    "../ttbox.sty"
   1.197 +    "../proof.sty"
   1.198 +    "../manual.bib"
   1.199 +    "../Logics/document/syntax.tex"
   1.200 +    "document/build"
   1.201 +    "document/root.tex"
   1.202 +
   1.203 +session Main (doc) in "Main" = HOL +
   1.204 +  options [document_variants = "main"]
   1.205 +  theories Main_Doc
   1.206 +  files
   1.207 +    "../prepare_document"
   1.208 +    "../pdfsetup.sty"
   1.209 +    "document/build"
   1.210 +    "document/root.tex"
   1.211 +
   1.212 +session Nitpick (doc) in "Nitpick" = Pure +
   1.213 +  options [document_variants = "nitpick"]
   1.214 +  theories
   1.215 +  files
   1.216 +    "../prepare_document"
   1.217 +    "../pdfsetup.sty"
   1.218 +    "../iman.sty"
   1.219 +    "../manual.bib"
   1.220 +    "document/build"
   1.221 +    "document/root.tex"
   1.222 +
   1.223 +session ProgProve (doc) in "ProgProve" = HOL +
   1.224 +  options [document_variants = "prog-prove", show_question_marks = false]
   1.225 +  theories
   1.226 +    Basics
   1.227 +    Bool_nat_list
   1.228 +    MyList
   1.229 +    Types_and_funs
   1.230 +    Logic
   1.231 +    Isar
   1.232 +  files
   1.233 +    "../prepare_document"
   1.234 +    "../pdfsetup.sty"
   1.235 +    "document/bang.eps"
   1.236 +    "document/bang.pdf"
   1.237 +    "document/build"
   1.238 +    "document/intro-isabelle.tex"
   1.239 +    "document/mathpartir.sty"
   1.240 +    "document/prelude.tex"
   1.241 +    "document/root.bib"
   1.242 +    "document/root.tex"
   1.243 +    "document/svmono.cls"
   1.244 +
   1.245 +session Ref (doc) in "Ref" = Pure +
   1.246 +  options [document_variants = "ref"]
   1.247 +  theories
   1.248 +  files
   1.249 +    "../prepare_document"
   1.250 +    "../pdfsetup.sty"
   1.251 +    "../iman.sty"
   1.252 +    "../extra.sty"
   1.253 +    "../ttbox.sty"
   1.254 +    "../proof.sty"
   1.255 +    "../manual.bib"
   1.256 +    "document/build"
   1.257 +    "document/classical.tex"
   1.258 +    "document/root.tex"
   1.259 +    "document/simplifier.tex"
   1.260 +    "document/substitution.tex"
   1.261 +    "document/syntax.tex"
   1.262 +    "document/tactic.tex"
   1.263 +    "document/thm.tex"
   1.264 +
   1.265 +session Sledgehammer (doc) in "Sledgehammer" = Pure +
   1.266 +  options [document_variants = "sledgehammer"]
   1.267 +  theories
   1.268 +  files
   1.269 +    "../prepare_document"
   1.270 +    "../pdfsetup.sty"
   1.271 +    "../iman.sty"
   1.272 +    "../manual.bib"
   1.273 +    "document/build"
   1.274 +    "document/root.tex"
   1.275 +
   1.276 +session System (doc) in "System" = Pure +
   1.277 +  options [document_variants = "system", thy_output_source]
   1.278 +  theories
   1.279 +    Basics
   1.280 +    Interfaces
   1.281 +    Sessions
   1.282 +    Presentation
   1.283 +    Scala
   1.284 +    Misc
   1.285 +  files
   1.286 +    "../prepare_document"
   1.287 +    "../IsarRef/document/style.sty"
   1.288 +    "../pdfsetup.sty"
   1.289 +    "../iman.sty"
   1.290 +    "../extra.sty"
   1.291 +    "../ttbox.sty"
   1.292 +    "../isar.sty"
   1.293 +    "../underscore.sty"
   1.294 +    "../manual.bib"
   1.295 +    "document/browser_screenshot.eps"
   1.296 +    "document/browser_screenshot.png"
   1.297 +    "document/build"
   1.298 +    "document/root.tex"
   1.299 +
   1.300 +session Tutorial (doc) in "Tutorial" = HOL +
   1.301 +  options [document_variants = "tutorial", print_mode = "brackets"]
   1.302 +  theories [thy_output_indent = 5]
   1.303 +    "ToyList/ToyList"
   1.304 +    "Ifexpr/Ifexpr"
   1.305 +    "CodeGen/CodeGen"
   1.306 +    "Trie/Trie"
   1.307 +    "Datatype/ABexpr"
   1.308 +    "Datatype/unfoldnested"
   1.309 +    "Datatype/Nested"
   1.310 +    "Datatype/Fundata"
   1.311 +    "Fun/fun0"
   1.312 +    "Advanced/simp2"
   1.313 +    "CTL/PDL"
   1.314 +    "CTL/CTL"
   1.315 +    "CTL/CTLind"
   1.316 +    "Inductive/Even"
   1.317 +    "Inductive/Mutual"
   1.318 +    "Inductive/Star"
   1.319 +    "Inductive/AB"
   1.320 +    "Inductive/Advanced"
   1.321 +    "Misc/Tree"
   1.322 +    "Misc/Tree2"
   1.323 +    "Misc/Plus"
   1.324 +    "Misc/case_exprs"
   1.325 +    "Misc/fakenat"
   1.326 +    "Misc/natsum"
   1.327 +    "Misc/pairs2"
   1.328 +    "Misc/Option2"
   1.329 +    "Misc/types"
   1.330 +    "Misc/prime_def"
   1.331 +    "Misc/simp"
   1.332 +    "Misc/Itrev"
   1.333 +    "Misc/AdvancedInd"
   1.334 +    "Misc/appendix"
   1.335 +  theories
   1.336 +    "Protocol/NS_Public"
   1.337 +    "Documents/Documents"
   1.338 +  theories [document = ""]
   1.339 +    "Types/Setup"
   1.340 +  theories [pretty_margin = 64, thy_output_indent = 0]
   1.341 +    "Types/Numbers"
   1.342 +    "Types/Pairs"
   1.343 +    "Types/Records"
   1.344 +    "Types/Typedefs"
   1.345 +    "Types/Overloading"
   1.346 +    "Types/Axioms"
   1.347 +    "Rules/Basic"
   1.348 +    "Rules/Blast"
   1.349 +    "Rules/Force"
   1.350 +  theories [pretty_margin = 64, thy_output_indent = 5]
   1.351 +    "Rules/Primes"
   1.352 +    "Rules/Forward"
   1.353 +    "Rules/Tacticals"
   1.354 +    "Rules/find2"
   1.355 +    "Sets/Examples"
   1.356 +    "Sets/Functions"
   1.357 +    "Sets/Relations"
   1.358 +    "Sets/Recur"
   1.359 +  files
   1.360 +    "ToyList/ToyList1"
   1.361 +    "ToyList/ToyList2"
   1.362 +    "../pdfsetup.sty"
   1.363 +    "../proof.sty"
   1.364 +    "../ttbox.sty"
   1.365 +    "../manual.bib"
   1.366 +    "document/advanced0.tex"
   1.367 +    "document/appendix0.tex"
   1.368 +    "document/basics.tex"
   1.369 +    "document/build"
   1.370 +    "document/cl2emono-modified.sty"
   1.371 +    "document/ctl0.tex"
   1.372 +    "document/documents0.tex"
   1.373 +    "document/fp.tex"
   1.374 +    "document/inductive0.tex"
   1.375 +    "document/isa-index"
   1.376 +    "document/Isa-logics.eps"
   1.377 +    "document/Isa-logics.pdf"
   1.378 +    "document/numerics.tex"
   1.379 +    "document/pghead.eps"
   1.380 +    "document/pghead.pdf"
   1.381 +    "document/preface.tex"
   1.382 +    "document/protocol.tex"
   1.383 +    "document/root.tex"
   1.384 +    "document/rules.tex"
   1.385 +    "document/sets.tex"
   1.386 +    "document/tutorial.sty"
   1.387 +    "document/typedef.pdf"
   1.388 +    "document/typedef.ps"
   1.389 +    "document/types0.tex"
   1.390 +