Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :

Commit 9c3fc6c4 authored by BOLDO Sylvie's avatar BOLDO Sylvie

Change of stating of canonic_exp_ge

parent b3738592
......@@ -303,7 +303,7 @@ Qed.
Theorem canonic_exp_ge:
forall prec,
(forall e, (e-prec <= fexp e)%Z) ->
(forall e, (e-fexp e <= prec)%Z) ->
(* OK with FLX, FLT and FTZ *)
forall x, generic_format x ->
(Rabs x < bpow (prec + canonic_exponent x))%R.
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