chapter AFP

session Polynomial_Commitment_Schemes = CryptHOL +
  options [timeout = 1200]
  sessions 
    "Sigma_Commit_Crypto"
    "Berlekamp_Zassenhaus"
    "Elimination_Of_Repeated_Factors"
    "Polynomial_Interpolation"
    "HOL-Computational_Algebra"
    "HOL-Number_Theory"

theories
    "Pairing"
    "Primitives"
    "DL_assumption"
    "tDL_assumption"
    "tSDH_assumption"
    "tBSDH_assumption"
    "Polynomial_Commitment_Schemes"
    "Algebraic_Group_Model"
    "KZG_def"
    "KZG_correct"
    "KZG_poly_bind"
    "KZG_eval_bind"
    "KZG_knowledge_sound"
    "KZG_hiding"
    "BatchKZG_def"
    "BatchKZG_correct"
    "BatchKZG_poly_bind"
    "BatchKZG_eval_bind"
    "BatchKZG_knowledge_sound"
  document_files
    "root.tex"
    "root.bib"