ROOT

session "tsp" = HOL +
  options[document=pdf, document_output="output"]
  sessions
    "HOL-Library"
    "HOL-Data_Structures"
    "HOL-Hoare"
    "Prim_Dijkstra_Simple"

  directories
    "adaptors"
    "algorithms"
    "berge"
    "graphs"
    "misc"
    "problems"
    "reductions"

  theories[quick_and_dirty, document=false]
    "graphs/MultiGraph"
    "adaptors/BergePrimAdaptor"
    
    "reductions/VertexCover4ToMetricTravelingSalesman_Specs"
    "reductions/FindHamiltonianPath"

  theories[document=false]
    "misc/Misc"
    "misc/Select"    

    "graphs/WeightedGraph"
    "graphs/CompleteGraph"
    "problems/MinWeightMatching"
    "problems/MinSpanningTree"
    "problems/EulerianTour"
    "problems/TravelingSalesman"
    "algorithms/DoubleTree"
    "algorithms/ChristofidesSerdyukov"
    "graphs/GraphAdjList"
    "graphs/GraphAdjMap_Specs"
    "reductions/VertexCover4ToMetricTravelingSalesman_AdjList"

  theories
    "Report"

  document_files
    "root.bib"
    "root.tex"