Commit bfeec30c authored by BOLDO Sylvie's avatar BOLDO Sylvie

NEWS pour la 2.5

parent 1d5a4239
Version 2.5.0:
- iter_pos?
- LPO (?)
- new definition of the ulp. ulp(0) is now 0 when there is no minimal
exponent, such as in FLX, and beta^(fexp n) when there is a n such
that n <= fexp n. For instance, the value of ulp(O) is then
beta^emin in FIX and FLT. The main lemma to use is ulp_neq_0 that
is equivalent to the previous "unfold ulp" provided the value is
not zero.
- added several lemmas in Fcore_ulp, including generic_format_ulp
- changed ulp_le: it now works for any values. Please use ulp_le_pos
for the previous behavior.
- changed ulp_error: it now requires x to be non zero, as ulp(0)
may now be zero.
- pred has been renamed pred_pos
- defined a predecessor and successor on both positive, negative and
zero values.
- added useful lemmas about pred and succ, including
generic_format_pred, succ_le_lt, le_pred_lt, succ_pred, pred_inj,
pred_monotone, pred_UP_eq_DN.
Version 2.4.0:
- moved some lemmas from Fcalc_digits to Fcore_digits and made them axiom-free
- added theorems about double rounding being innocuous (Fappli_double_round.v)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment