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 (\Add\) @@ -1167,7 +1167,7 @@ end -bundle no_floatarith_notation +bundle no_floatarith_syntax begin no_notation Add (\Add\)