diff --git a/BonnAnalysis.lean b/BonnAnalysis.lean
index a3ff7b2..c34c78c 100644
--- a/BonnAnalysis.lean
+++ b/BonnAnalysis.lean
@@ -1,8 +1,15 @@
 import BonnAnalysis.ComplexInterpolation
+import BonnAnalysis.ConvergingSequences
+import BonnAnalysis.ConvolutionTendsToUniformly
+import BonnAnalysis.Distributions
+import BonnAnalysis.DistributionsExamples
+import BonnAnalysis.DistributionsOfVEndo
 import BonnAnalysis.Dual
 import BonnAnalysis.Examples
+import BonnAnalysis.Hadamard
 import BonnAnalysis.LorentzSpace
 import BonnAnalysis.Plancherel
 import BonnAnalysis.RealInterpolation
 import BonnAnalysis.StrongType
 import BonnAnalysis.Test
+import BonnAnalysis.UniformConvergenceSequences
diff --git a/BonnAnalysis/Dual.lean b/BonnAnalysis/Dual.lean
index f222eaf..5466de6 100644
--- a/BonnAnalysis/Dual.lean
+++ b/BonnAnalysis/Dual.lean
@@ -7,12 +7,6 @@ import Mathlib.Analysis.NormedSpace.LinearIsometry
 import Mathlib.MeasureTheory.Integral.Bochner
 import Mathlib.Data.Real.Sign
 
-
-set_option linter.setOption false
-set_option trace.profiler true
-set_option profiler true
-
-
 /-! We show that the dual space of `L^p` for `1 ≤ p < ∞`.
 
 See [Stein-Shakarchi, Functional Analysis, section 1.4] -/