Summary
- use poly_of_list from Polynomial.thy, renamed list_to_poly_f to poly_of_list_f
The file was modified | thys/Polynomial_Factorization/Berlekamp_Hensel_Factorization.thy (diff) |
The file was modified | thys/Polynomial_Factorization/Factorization_Oracle.thy (diff) |
The file was modified | thys/Polynomial_Factorization/Polynomial_Field.thy (diff) |