
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 \<equiv> f \<sim>[at_top] g"
 
-bundle asymp_equiv_notation
+bundle asymp_equiv_syntax
 begin
 notation asymp_equiv_at_top (infix \<open>\<sim>\<close> 50)
 end




