From 39bfa90d2bc53d4403962267da4c6ecbe26c3129 Mon Sep 17 00:00:00 2001
From: gmelquio
Date: Fri, 11 Sep 2009 13:24:12 +0000
Subject: Added the following lemmas to homogenize Reals a bit: -
 Rmult_eq_compat_r, Rmult_eq_reg_r, Rplus_le_reg_r, Rmult_lt_reg_r,  
 Rmult_le_reg_r (mirrored variants of the existing _l lemmas); - minus_IZR,
 opp_IZR (Ropp_Ropp_IZR), abs_IZR (mirrored Rabs_Zabs); - Rle_abs (RRle_abs);
 - Zpower_pos_powerRZ (signed variant of Zpower_nat_powerRZ).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12321 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES | 1 +
 1 file changed, 1 insertion(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 70f183d15b..6335a6b1d7 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
 =========================
-- 
cgit v1.2.3