
diff -r 849efff7de15 -r ad5fc948e053 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Wed Oct 02 22:08:52 2024 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Oct 02 23:47:07 2024 +0200
@@ -1143,7 +1143,7 @@
 
 section "Avoid pollution of name space"
 
-bundle floatarith_notation
+bundle floatarith_syntax
 begin
 
 notation Add (\<open>Add\<close>)
@@ -1167,7 +1167,7 @@
 
 end
 
-bundle no_floatarith_notation
+bundle no_floatarith_syntax
 begin
 
 no_notation Add (\<open>Add\<close>)




