chapter AFP

session Virtual_Substitution = "HOL-Analysis" +
  options [timeout = 1800]
  sessions
    "Polynomials"
  theories
    QE

    MPolyExtension
      ExecutiblePolyProps

    PolyAtoms

    Debruijn
      Reindex

    Optimizations
      OptimizationProofs

    VSAlgos
      Heuristic
      Exports
    
    LinearCase
      QuadraticCase
      EliminateVariable
      LuckyFind
      EqualityVS

    UniAtoms
      NegInfinity
        NegInfinityUni
      Infinitesimals
        InfinitesimalsUni
      DNFUni
        GeneralVSProofs

    DNF
      VSQuad
      HeuristicProofs
      ExportProofs
  theories [document = false]
    PrettyPrinting
  document_files
    "root.tex"
    "root.bib"