src/HOL/Decision_Procs/Approximation.thy
changeset 81107 ad5fc948e053
parent 81100 6ae3d0b2b8ad
child 81116 0fb1e2dd4122
--- 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>)