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/Rtrigo_calc.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/Rtrigo_calc.v')
| -rw-r--r-- | theories/Reals/Rtrigo_calc.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v index 587c2424a..40989418c 100644 --- a/theories/Reals/Rtrigo_calc.v +++ b/theories/Reals/Rtrigo_calc.v @@ -9,7 +9,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. -Require Import Rtrigo. +Require Import Rtrigo1. Require Import R_sqrt. Open Local Scope R_scope. |