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