doc-src/ROOT
changeset 48966 6e15de7dd871
parent 48963 f11d88bfa934
child 48968 5e83c70266cf
--- a/doc-src/ROOT	Tue Aug 28 13:15:15 2012 +0200
+++ b/doc-src/ROOT	Tue Aug 28 14:37:57 2012 +0200
@@ -278,9 +278,7 @@
     "document/root.tex"
 
 session Tutorial (doc) in "TutorialI" = HOL +
-  options [browser_info = false, document = false,
-    document_dump = document, document_dump_mode = "tex",
-    print_mode = "brackets"]
+  options [document_variants = "tutorial", print_mode = "brackets"]
   theories [thy_output_indent = 5]
     "ToyList/ToyList"
     "Ifexpr/Ifexpr"
@@ -317,7 +315,7 @@
   theories
     "Protocol/NS_Public"
     "Documents/Documents"
-  theories [document_dump = ""]
+  theories [document = ""]
     "Types/Setup"
   theories [pretty_margin = 64, thy_output_indent = 0]
     "Types/Numbers"
@@ -338,8 +336,15 @@
     "Sets/Functions"
     "Sets/Relations"
     "Sets/Recur"
+  files
+    "ToyList/ToyList1"
+    "ToyList/ToyList2"
+    "../pdfsetup.sty"
+    "../proof.sty"
+    "../ttbox.sty"
+    "../manual.bib"
+    "document/pghead.eps"
+    "document/pghead.pdf"
+    "document/build"
+    "document/root.tex"
 
-session "HOL-ToyList2" (doc) in "TutorialI/ToyList2" = HOL +
-  options [browser_info = false, document = false, print_mode = "brackets"]
-  theories ToyList
-