src/HOL/Library/Landau_Symbols.thy
changeset 81107 ad5fc948e053
parent 80653 b98f1057da0e
child 81142 6ad2c917dd2e
--- 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