diff options
| author |  bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-11 15:32:59 +0000 |
|---|---|---|
| committer | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-11 15:32:59 +0000 |
| commit | 4dab5938805ec41237b1bdce5efa308e37932cd0 (patch) | |
| tree | 617c1bfabe41e2e99d0dbefe305b170745edf811 /theories/Reals/Machin.v | |
| parent | a5c2bbab10ba5f26ad289e1b911db69294946c55 (diff) | |
finish the rearrangement for removing the sin_PI2 axiom. This new version
- provides the atan function
- shows that this function is equal between -1 and 1 to a function defined
with power series
- establishes the equality with the PI value as given by the alternated
series constructed with PI_tg
- provides a smarter theorem to compute approximations of PI, based on a
formula in the same family as the one used by John Machin in 1706
Dependencies between files have been rearranged so that the new theorems
are loaded with the library Reals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15429 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Machin.v')
| -rw-r--r-- | theories/Reals/Machin.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/Machin.v b/theories/Reals/Machin.v index 96f7cae8c..503e79a40 100644 --- a/theories/Reals/Machin.v +++ b/theories/Reals/Machin.v @@ -1,7 +1,7 @@ Require Import Fourier. Require Import Rbase. -Require Import Rtrigo. -Require Import Ranalysis. +Require Import Rtrigo1. +Require Import Ranalysis_reg. Require Import Rfunctions. Require Import AltSeries. Require Import Rseries. |