diff options
| author |  gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-11 13:24:12 +0000 |
|---|---|---|
| committer | gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-11 13:24:12 +0000 |
| commit | 39bfa90d2bc53d4403962267da4c6ecbe26c3129 (patch) | |
| tree | 6142a7b573f4b53adcd66f50d80eaf58646ca451 /library/nametab.mli | |
| parent | a37c28e3b76f921e377dccca639c6ffa5331eefc (diff) | |
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
Diffstat (limited to 'library/nametab.mli')
0 files changed, 0 insertions, 0 deletions