doc-src/ROOT
changeset 48526 4372b7cb858d
parent 48516 c5d0f19ef7cb
child 48578 21361b6189a6
--- a/doc-src/ROOT	Thu Jul 26 19:16:04 2012 +0200
+++ b/doc-src/ROOT	Thu Jul 26 19:40:19 2012 +0200
@@ -115,7 +115,65 @@
     Presentation
     Misc
 
-(* session Tutorial (doc) in "Tutorial" = HOL + FIXME *)
+session Tutorial (doc) in "TutorialI" = HOL +
+  options [browser_info = false, document = false,
+    document_dump = document, document_dump_mode = "tex",
+    print_mode = "brackets", threads = 1 (* FIXME *)]
+  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
+    "Types/Numbers"
+    "Types/Pairs"
+    "Types/Records"
+    "Types/Typedefs"
+    "Types/Overloading"
+    "Types/Axioms"
+    "Rules/Basic"
+    "Rules/Blast"
+    "Rules/Force"
+    "Rules/Forward"
+    "Rules/Tacticals"
+    "Rules/find2"
+    "Sets/Examples"
+    "Sets/Functions"
+    "Sets/Relations"
+    "Sets/Recur"
 
 session examples (doc) in "ZF" = ZF +
   options [browser_info = false, document = false,