src/Doc/ROOT
changeset 72103 7b318273a4aa
parent 72006 751f371d6883
child 72255 dc51115fa4aa
equal deleted inserted replaced
72101:c65614b556b2 72103:7b318273a4aa
   376   document_files
   376   document_files
   377     "build"
   377     "build"
   378     "root.tex"
   378     "root.tex"
   379 
   379 
   380 session System (doc) in "System" = Pure +
   380 session System (doc) in "System" = Pure +
   381   options [document_variants = "system", thy_output_source, pide_session]
   381   options [document_variants = "system", thy_output_source]
   382   sessions
   382   sessions
   383     "HOL-Library"
   383     "HOL-Library"
   384   theories
   384   theories
   385     Environment
   385     Environment
   386     Sessions
   386     Sessions