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,