From 6e3d6ceeee97e532a4ef3bb5952ce3051a0ac151 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Mon, 6 Jan 2025 12:11:45 -0500 Subject: [PATCH] add fix from Bhavik Mehta; closes #236 --- .../S01_Elementary_Integration.lean | 2 -- 1 file changed, 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 index cb7f5171..034134d2 100644 --- 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