1 files changed, 1 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 70f183d15..6335a6b1d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -76,6 +76,7 @@ Library
 - The function Compare_dec.nat_compare is now defined directly,
   instead of relying on lt_eq_lt_dec. The earlier version is still
   available under the name nat_compare_alt.
+- Lemmas in library Reals have been homogenized a bit.
 
 Changes from V8.1 to V8.2
 =========================