diff options
| author | Michael Soegtrop | 2019-09-07 07:34:50 +0200 |
|---|---|---|
| committer | Michael Soegtrop | 2020-04-01 16:13:30 +0200 |
| commit | 934c757b72fa9fdae5828068c7e8a050d1103a10 (patch) | |
| tree | 245bb959f5c17177572e3478096ab4518e3a796e /doc/stdlib | |
| parent | aa9926492feaf8326f379469a555f77393fcd306 (diff) | |
- Adjusted definitions and lemmas for asin and acos to what has been discussed
- Added derivative for asin and acos
- Added a few additional trigonometry lemmas
- Added Lemmas for the derivative of a decreasing inverse function
- Did some cleanup (move lemmas to the files where they belong)
Diffstat (limited to 'doc/stdlib')
| -rw-r--r-- | doc/stdlib/index-list.html.template | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index e64b4be454..7fa621c11c 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -558,6 +558,7 @@ through the <tt>Require Import</tt> command.</p> theories/Reals/Rtrigo_fun.v theories/Reals/Rtrigo1.v theories/Reals/Rtrigo.v + theories/Reals/Rtrigo_facts.v theories/Reals/Ratan.v theories/Reals/Machin.v theories/Reals/SplitAbsolu.v |