chapter AFP

session Submodular_Greedy = HOL +
  options [timeout = 300]
  sessions
    "HOL-Library"
    "HOL-Analysis"
  directories
    "Core"
    "Algorithms"
    "Proofs"
  theories
    "Core/Submodular_Base"

    "Algorithms/Greedy_Submodular_Construct"
    "Algorithms/Lazy_Greedy_Oracle"
    "Algorithms/Lazy_Greedy_Stateful"

    "Proofs/Greedy_Step_Spec"
    "Proofs/Greedy_Submodular_Approx"
    "Proofs/Lazy_Greedy_Stateful_StepSpec"
    "Proofs/Lazy_Greedy_Stateful_Approx"
  document_files
    "root.tex"
    "root.bib"