fix changelog

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -103,67 +103,6 @@
 
 - in `lebesgue_integrable.v`:
   + lemma `integrable_set0`
-- in `probability.v`:
-  + definition `ccdf`
-  + lemmas `lebesgue_stieltjes_cdf_id`, `cdf_ccdf_1`, `ccdf_nonincreasing`, `cvg_ccdfy0`, `cvg_ccdfNy1`, `ccdf_right_continuous`, `ge0_expectation_ccdf`
-  + corollaries `ccdf_cdf_1`, `ccdf_1_cdf`, `cdf_1_ccdf`
-
-- in `num_normedtype.v`:
-  + lemma `nbhs_infty_gtr`
-- in `function_spaces.v`:
-  + lemmas `cvg_big`, `continuous_big`
-
-- in `realfun.v`:
-  + lemma `cvg_addrl_Ny`
-
-- in `constructive_ereal.v`:
-  + lemmas `mule_natr`, `dmule_natr`
-  + lemmas `inve_eqy`, `inve_eqNy`
-
-- in `uniform_structure.v`:
-  + lemma `continuous_injective_withinNx`
-
-- in `constructive_ereal.v`:
-  + variants `Ione`, `Idummy_placeholder`
-  + inductives `Inatmul`, `IEFin`
-  + definition `parse`, `print`
-  + number notations in scopes `ereal_dual_scope` and `ereal_scope`
-  + notation `- 1` in scopes `ereal_dual_scope` and `ereal_scope`
-- in `pseudometric_normed_Zmodule.v`:
-  + lemma `le0_ball0`
-- in `theories/landau.v`:
-  + lemma `littleoE0`
-
-- in `constructive_ereal.v`:
-  + lemma `lt0_adde`
-
-- in `unstable.v`
-  + lemmas `coprime_prodr`, `Gauss_dvd_prod`, `expn_prod`, `mono_leq_infl`,
-    `card_big_setU`
-
-- file `pnt.v`
-  + definitions `next_prime`, `prime_seq`
-  + lemmas `leq_prime_seq`, `mem_prime_seq`
-  + theorem `dvg_sum_inv_prime_seq`
-- new directory `theories/measure_theory` with new files:
-  + `measurable_structure.v`
-  + `measure_function.v`
-  + `counting_measure.v`
-  + `dirac_measure.v`
-  + `probability_measure.v`
-  + `measure_negligible.v`
-  + `measure_extension.v`
-  + `measurable_function.v`
-  + `measure.v`
-
-- in `realfun.v`:
-  + lemmas `derivable_oy_continuous_within_itvcy`,
-           `derivable_oy_continuous_within_itvNyc`
-  + lemmas `derivable_oo_continuousW`,
-           `derivable_oy_continuousWoo`,
-           `derivable_oy_continuousW`,
-           `derivable_Nyo_continuousWoo`,
-           `derivable_Nyo_continuousW`
 
 - in `measurable_function.v`:
   + lemma `preimage_set_system_compS`
@@ -303,18 +242,6 @@
 
 - in `charge.v`:
   + `induced` -> `induced_charge`
-- in `reals.v`:
-  + `sup_le_ub` -> `ge_sub`
-  + `le_inf` -> `inf_le`
-  + `le_sup` -> `sup_le`
-  + `sup_ubound` -> `ub_le_sup`
-  + `inf_lbound` -> `ge_inf`
-  + `ub_ereal_sup` -> `ge_ereal_sup`
-  + `ereal_inf_le` -> `ge_ereal_inf`
-  + `le_ereal_sup` -> `ereal_sup_le`
-  + `le_ereal_inf` -> `ereal_inf_le_tmp`
-  + `lb_ereal_inf` -> `le_ereal_inf_tmp`
-  + `ereal_sup_ge` -> `le_ereal_sup_tmp`
 
 ### Generalized
 
@@ -399,8 +326,6 @@
 
 - in `set_interval.v`:
   + lemma `interval_set1` (use `set_itv1` instead)
-- in `ereal.v`:
-  + notation `ereal_sup_le` (was deprecated since 1.11.0)
 
 ### Infrastructure