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>)