chapter AFP

session Refine_Monadic (AFP) = Automatic_Refinement +
  options [timeout = 1200, document_variants = "document:outline=/proof,/ML"]
  theories [document = false]
    "~~/src/HOL/Library/While_Combinator"
    "~~/src/HOL/Library/Lattice_Syntax"
    "~~/src/HOL/Library/Monad_Syntax"
    "~~/src/HOL/Word/Word"
  theories
    Refine_Monadic
    "examples/Examples"
  document_files
    "root.bib"
    "root.tex"
