Def Mathlib.Tactic.removeRanges

Modification history

2025-11-18 10:56
Mathlib/Tactic/Linter/FindDeprecations.lean
chore: bump toolchain to v4.26.0-rc1 (#31763)
Modified Mathlib.Tactic.removeRangesView on Github →
2025-10-21 16:00
Mathlib/Tactic/Linter/FindDeprecations.lean
CI: remove deprecations automatically (#30070) …
Added Mathlib.Tactic.removeRangesView on Github →