session Grat_Check = Sepref_IICF +
  options [document = pdf, document_output = "output",
    document_variants = "document:outline=/proof,/ML"]

  theories [document = false]
    "Refine_Imperative_HOL.Sepref_ICF_Bindings"
    DRAT_Misc
    Exc_Nres_Monad
    Synth_Definition
    Dynamic_Array
    Array_Map_Default
    Parser_Iterator


  theories
    SAT_Basic
    Unit_Propagation 
    Grat_Basic
    
  theories [document = false]
    Unsat_Check        (* TODO: Discontinue? *)
    Unsat_Check_Split  (* TODO: Discontinue *)
  theories
    Unsat_Check_Split_MM
    Sat_Check
    Grat_Check_Code_Exporter
    
  theories [document = false]
    Cert_Sat
    
  document_files
    "root.tex"
