session "avl-verification" = "Aeneas" +
  options [document = pdf, document_output = "output"]
  theories
    Notraits
    Verification
  document_files
    "root.tex"