diff -r 849efff7de15 -r ad5fc948e053 src/HOL/Computational_Algebra/Polynomial_FPS.thy --- a/src/HOL/Computational_Algebra/Polynomial_FPS.thy Wed Oct 02 22:08:52 2024 +0200 +++ b/src/HOL/Computational_Algebra/Polynomial_FPS.thy Wed Oct 02 23:47:07 2024 +0200 @@ -9,7 +9,7 @@ begin context - includes fps_notation + includes fps_syntax begin definition fps_of_poly where