chapter AFP

session Berlekamp_Zassenhaus = Subresultants +
  description "Berlekamp-Zassenhaus's Factorization Algorithm"
  options [timeout = 1200]
  sessions
    "HOL-Number_Theory"
    "HOL-Types_To_Sets"
    Polynomial_Factorization
    Polynomial_Interpolation
    "Efficient-Mergesort"
    Native_Word
    Show
  theories
    (* Arithmetic for Finite Fields *)
    Finite_Field
    Finite_Field_Record_Based
    Arithmetic_Record_Based
    Matrix_Record_Based
    Poly_Mod
    Poly_Mod_Finite_Field
    Poly_Mod_Finite_Field_Record_Based
    Polynomial_Record_Based
    (* Berlekamp's Factorization Algorithm *)
    Chinese_Remainder_Poly
    Berlekamp_Type_Based
    Distinct_Degree_Factorization
    Finite_Field_Factorization_Record_Based
    (* Hensel Lifting *)
    Hensel_Lifting_Type_Based
    Hensel_Lifting
    Berlekamp_Hensel
    (* Zassenhaus Reconstruction *)
    Square_Free_Int_To_Square_Free_GFp
    Suitable_Prime
    Degree_Bound
    Mahler_Measure
    Factor_Bound
    Sublist_Iteration
    Reconstruction
    (* An Efficient Algorithm for Integer Polynomials *)
    Berlekamp_Zassenhaus
    Square_Free_Factorization_Int
    Factorize_Int_Poly
    Factorize_Rat_Poly
    Factorization_External_Interface
  document_files
    "algorithm2e.sty"
    "root.bib"
    "root.tex"