src/HOL/Computational_Algebra/Polynomial_FPS.thy
changeset 81107 ad5fc948e053
parent 69597 ff784d5a5bfb
child 82530 904589510439
--- 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