add fix from Bhavik Mehta; closes #236

avigad · Jan 6, 2025 · 6e3d6ce · 6e3d6ce
1 parent c580810
commit 6e3d6ce
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/MIL/C12_Integration_and_Measure_Theory/S01_Elementary_Integration.lean b/MIL/C12_Integration_and_Measure_Theory/S01_Elementary_Integration.lean
@@ -3,8 +3,6 @@ import Mathlib.MeasureTheory.Integral.IntervalIntegral
 import Mathlib.Analysis.SpecialFunctions.Integrals
 import Mathlib.Analysis.Convolution
 
-local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y)
-
 open Set Filter
 
 open Topology Filter