theory Fact_Poly
imports
  Factorize_Int_Poly
begin

definition "poly_of = poly_of_list o map int_of_integer" 
definition "of_poly = map integer_of_int o coeffs" 

definition "factor_int_poly = 
    map_prod integer_of_int (map (map_prod of_poly (\<lambda> exp. integer_of_nat (exp + 1)))) 
  o factorize_int_poly o poly_of" 

export_code factor_int_poly in Haskell module_name Factor file Fact_Poly

end