diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 44428f71f..b5153bd4d 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -105,31 +105,6 @@
            `closureEbigcap`, `interiorEbigcup`,
 	   `closure_open_regclosed`, `interior_closed_regopen`,
 	   `closure_interior_idem`, `interior_closure_idem`
-- new directory `theories/topology` with new files:
-  + `topology.v`
-  + `bool_topology.v`
-  + `compact.v`
-  + `connected.v`
-  + `matrix_topology.v`
-  + `nat_topology.v`
-  + `order_topology.v`
-  + `product_topology.v`
-  + `pseudometric_structure.v`
-  + `subspace_topology.v`
-  + `supremum_topology.v`
-  + `topology_structure.v`
-  + `uniform_structure.v`
-  + `weak_topology.v`
-  + `num_topology.v`
-  + `quotient_topology.v`
-- in `lebesgue_measure.v`:
-  + lemmas `RintegralZl`, `RintegralZr`, `Rintegral_ge0`
-
-- in `trigo.v`:
-  + lemmas `derive1_atan`, `lt_atan`, `le_atan`, `cvgy_atan`
-
-- in `exp.v`:
-  + lemmas `cvgr_expR`, `cvgn_expR`
 
 - in file `topology_structure.v`,
   + mixin `isContinuous`, type `continuousType`, structure `Continuous`
@@ -137,13 +112,13 @@
   + new definition `mkcts`.
 
 - in file `subspace_topology.v`,
-  + new lemmas `continuous_subspace_setT`, `nbhs_prodX_subspace_inE`, and 
+  + new lemmas `continuous_subspace_setT`, `nbhs_prodX_subspace_inE`, and
     `continuous_subspace_prodP`.
   + type `continuousFunType`, HB structure `ContinuousFun`
 
 - in file `subtype_topology.v`,
-  + new lemmas `subspace_subtypeP`, `subspace_sigL_continuousP`, 
-    `subspace_valL_continuousP'`, `subspace_valL_continuousP`, `sigT_of_setXK`, 
+  + new lemmas `subspace_subtypeP`, `subspace_sigL_continuousP`,
+    `subspace_valL_continuousP'`, `subspace_valL_continuousP`, `sigT_of_setXK`,
     `setX_of_sigTK`, `setX_of_sigT_continuous`, and `sigT_of_setX_continuous`.
 
 ### Changed