chapter AFP

session Sturm_Sequences = "HOL-Computational_Algebra" +
  options [timeout = 600, document_logo,
    document_variants = "document:outline=/proof,/ML:userguide"]
  sessions
    "Pure-ex"
  directories
    "Lib"
    "Examples"
  theories
    "Lib/Sturm_Library_Document"
    "Lib/Misc_Polynomial"
  theories [document = false]
    "Lib/Sturm_Library"
  theories
    Sturm_Theorem
    Sturm_Method
    "Examples/Sturm_Ex"
  document_files
    "root.tex"
    "root_userguide.tex"