Quelle  ROOT

(* All sessions must be in chapter AFP *)
chapter AFP

session "Differential_Privacy" = "HOL-Probability" +
  options [timeout = 600]

directories "List_Space"
theories[document=false]
  "List_Space/Measurable_Isomorphism"
  "List_Space/Source_and_Sink_Algebras"
  "List_Space/Source_and_Sink_Algebras_Constructions"

theories
  "List_Space/List_Space"

theories
  "L1_norm_list"

theories[document=false]
  "Additional_Lemmas_for_Calculation"
  "Additional_Lemmas_for_Integrals"

theories
  "Laplace_Distribution"

theories
  "Comparable_Probability_Measures"
  "Differential_Privacy_Divergence"
  "Differential_Privacy_Randomized_Response"
  "Differential_Privacy_Laplace_Mechanism"
  "Differential_Privacy_Laplace_Mechanism_Multi"
  "Differential_Privacy_Standard"
  "Differential_Privacy_Example_Report_Noisy_Max"

document_files
  "root.tex"
  "root.bib"