lib/isabelle/Why3_Real.thy · 33670484cac3907a1e963d0b075d515f2c3ed7bf · Why3 / why3 · GitLab

Find file Blame History Permalink

theory real.Trigonometry: replaced the insanely too precise bounds · 33670484
MARCHE Claude authored Oct 16, 2015
```
for pi by the best possible bounds in double-precision IEEE-754
floating-point numbers
```
33670484