src/Doc/ROOT
changeset 70678 36c8c32346cb
parent 70675 efd995488228
child 71099 20c1b9516d27
equal deleted inserted replaced
70677:56d70f7ce4a4 70678:36c8c32346cb
   402   document_files
   402   document_files
   403     "build"
   403     "build"
   404     "root.tex"
   404     "root.tex"
   405 
   405 
   406 session Tutorial (doc) in "Tutorial" = HOL +
   406 session Tutorial (doc) in "Tutorial" = HOL +
       
   407   options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
   407   directories "Advanced" "CTL" "CodeGen" "Datatype" "Documents" "Fun" "Ifexpr"
   408   directories "Advanced" "CTL" "CodeGen" "Datatype" "Documents" "Fun" "Ifexpr"
   408     "Inductive" "Misc" "Protocol" "Rules" "Sets" "ToyList" "Trie" "Types"
   409     "Inductive" "Misc" "Protocol" "Rules" "Sets" "ToyList" "Trie" "Types"
   409   options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
       
   410   theories [threads = 1]
   410   theories [threads = 1]
   411     "ToyList/ToyList_Test"
   411     "ToyList/ToyList_Test"
   412   theories [thy_output_indent = 5]
   412   theories [thy_output_indent = 5]
   413     "ToyList/ToyList"
   413     "ToyList/ToyList"
   414     "Ifexpr/Ifexpr"
   414     "Ifexpr/Ifexpr"