diff -r cccbfa567117 -r b69e4da2604b src/HOL/Computational_Algebra/Polynomial.thy --- a/src/HOL/Computational_Algebra/Polynomial.thy Fri Jun 06 18:36:29 2025 +0100 +++ b/src/HOL/Computational_Algebra/Polynomial.thy Mon Jun 09 22:14:38 2025 +0200 @@ -550,7 +550,7 @@ where [code]: "is_zero p \ List.null (coeffs p)" lemma is_zero_null [code_abbrev]: "is_zero p \ p = 0" - by (simp add: is_zero_def null_def) + by (simp add: is_zero_def) text \Reconstructing the polynomial from the list\