added session HOL-Tutorial;
authorwenzelm
Thu, 26 Jul 2012 19:40:19 +0200
changeset 495414372b7cb858d
parent 49540 a33784b07c6b
child 49542 4ee8d70cd5a3
added session HOL-Tutorial;
doc-src/ROOT
     1.1 --- a/doc-src/ROOT	Thu Jul 26 19:16:04 2012 +0200
     1.2 +++ b/doc-src/ROOT	Thu Jul 26 19:40:19 2012 +0200
     1.3 @@ -115,7 +115,65 @@
     1.4      Presentation
     1.5      Misc
     1.6  
     1.7 -(* session Tutorial (doc) in "Tutorial" = HOL + FIXME *)
     1.8 +session Tutorial (doc) in "TutorialI" = HOL +
     1.9 +  options [browser_info = false, document = false,
    1.10 +    document_dump = document, document_dump_mode = "tex",
    1.11 +    print_mode = "brackets", threads = 1 (* FIXME *)]
    1.12 +  theories [thy_output_indent = 5]
    1.13 +    "ToyList/ToyList"
    1.14 +    "Ifexpr/Ifexpr"
    1.15 +    "CodeGen/CodeGen"
    1.16 +    "Trie/Trie"
    1.17 +    "Datatype/ABexpr"
    1.18 +    "Datatype/unfoldnested"
    1.19 +    "Datatype/Nested"
    1.20 +    "Datatype/Fundata"
    1.21 +    "Fun/fun0"
    1.22 +    "Advanced/simp2"
    1.23 +    "CTL/PDL"
    1.24 +    "CTL/CTL"
    1.25 +    "CTL/CTLind"
    1.26 +    "Inductive/Even"
    1.27 +    "Inductive/Mutual"
    1.28 +    "Inductive/Star"
    1.29 +    "Inductive/AB"
    1.30 +    "Inductive/Advanced"
    1.31 +    "Misc/Tree"
    1.32 +    "Misc/Tree2"
    1.33 +    "Misc/Plus"
    1.34 +    "Misc/case_exprs"
    1.35 +    "Misc/fakenat"
    1.36 +    "Misc/natsum"
    1.37 +    "Misc/pairs2"
    1.38 +    "Misc/Option2"
    1.39 +    "Misc/types"
    1.40 +    "Misc/prime_def"
    1.41 +    "Misc/simp"
    1.42 +    "Misc/Itrev"
    1.43 +    "Misc/AdvancedInd"
    1.44 +    "Misc/appendix"
    1.45 +  theories
    1.46 +    "Protocol/NS_Public"
    1.47 +    "Documents/Documents"
    1.48 +  theories [document_dump = ""]
    1.49 +    "Types/Setup"
    1.50 +  theories
    1.51 +    "Types/Numbers"
    1.52 +    "Types/Pairs"
    1.53 +    "Types/Records"
    1.54 +    "Types/Typedefs"
    1.55 +    "Types/Overloading"
    1.56 +    "Types/Axioms"
    1.57 +    "Rules/Basic"
    1.58 +    "Rules/Blast"
    1.59 +    "Rules/Force"
    1.60 +    "Rules/Forward"
    1.61 +    "Rules/Tacticals"
    1.62 +    "Rules/find2"
    1.63 +    "Sets/Examples"
    1.64 +    "Sets/Functions"
    1.65 +    "Sets/Relations"
    1.66 +    "Sets/Recur"
    1.67  
    1.68  session examples (doc) in "ZF" = ZF +
    1.69    options [browser_info = false, document = false,