diff -r 849efff7de15 -r ad5fc948e053 src/HOL/Library/Landau_Symbols.thy --- a/src/HOL/Library/Landau_Symbols.thy Wed Oct 02 22:08:52 2024 +0200 +++ b/src/HOL/Library/Landau_Symbols.thy Wed Oct 02 23:47:07 2024 +0200 @@ -1741,7 +1741,7 @@ abbreviation (input) asymp_equiv_at_top where "asymp_equiv_at_top f g \ f \[at_top] g" -bundle asymp_equiv_notation +bundle asymp_equiv_syntax begin notation asymp_equiv_at_top (infix \\\ 50) end