diff -r a33784b07c6b -r 4372b7cb858d doc-src/ROOT --- 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,