diff options
| author |  bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-11 09:00:00 +0000 |
|---|---|---|
| committer | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-11 09:00:00 +0000 |
| commit | a5c2bbab10ba5f26ad289e1b911db69294946c55 (patch) | |
| tree | 86f47b8c5491f5e47230ef3d6422bd79e19d67fa /theories/Reals/vo.itarget | |
| parent | 791e5812a9fb4978a3c2f6aba0de8658e74d1597 (diff) | |
Adds the proof of PI_ineq, plus some other smarter ways to approximate PI
and of course, the definition of atan (the inverse of tan, from R to
(-PI/2, PI/2)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15428 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/vo.itarget')
| -rw-r--r-- | theories/Reals/vo.itarget | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/theories/Reals/vo.itarget b/theories/Reals/vo.itarget index bcd47a0b2..d575c34c4 100644 --- a/theories/Reals/vo.itarget +++ b/theories/Reals/vo.itarget @@ -9,6 +9,7 @@ DiscrR.vo Exp_prop.vo Integration.vo LegacyRfield.vo +Machin.vo MVT.vo NewtonInt.vo PartSum.vo @@ -17,7 +18,9 @@ Ranalysis1.vo Ranalysis2.vo Ranalysis3.vo Ranalysis4.vo +Ranalysis5.vo Ranalysis.vo +Ratan.vo Raxioms.vo Rbase.vo Rbasic_fun.vo |