chapter AFP

session Complex_Bounded_Operators(AFP) = "HOL-Analysis" +
  options [timeout = 2400]
  sessions
    "HOL-Examples"
    "HOL-Types_To_Sets"
    Jordan_Normal_Form
    Banach_Steinhaus
    Real_Impl
  directories
    extra
  theories
    Complex_L2
    Cblinfun_Code
    Cblinfun_Code_Examples
  document_files
    root.tex
    root.bib
