chapter AFP

session "BTree" (AFP) = "Refine_Imperative_HOL" +
  options [timeout = 1200]
  sessions
    "HOL-Data_Structures"
  theories
    BTree
    BTree_Height
    BTree_Set
    BTree_Split
  theories [condition = ISABELLE_OCAMLFIND]
    Array_SBlit
    Partially_Filled_Array
    BTree_Imp
    BTree_ImpSet
    BTree_ImpSplit
  document_files
    "root.tex"
    "root.bib"
