From 934c757b72fa9fdae5828068c7e8a050d1103a10 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop Date: Sat, 7 Sep 2019 07:34:50 +0200 Subject: - 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) --- doc/stdlib/index-list.html.template | 1 + 1 file changed, 1 insertion(+) (limited to 'doc/stdlib') 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 Require Import command.

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 -- cgit v1.2.3