Commit 2025-09-08 07:33 f1c28066
View on Github →chore: remove >6 month deprecations (#29276) This was mostly generated by the regex:
(^@\[deprecated.*since.*2025-02.*\]\n?\s*(noncomputable )?(protected )?alias\n?\s*[A-Za-z0-9_.'?!₀ℒ]+ :=\n?\s*[A-Za-z0-9_.'?!₀]+\n)+\n
which only handles alias. Manually reviewing theorems and defs seems reasonable at this point.