Commit 2025-12-29 03:44 1448aee2
View on Github →chore: remove May 2025 deprecated declarations (#33014) The first commit, like #32990, was done by script:
import Mathlib
import Archive
import Counterexamples
#clear_deprecations "2025-05-01" "2025-05-31" really