changeset 56370 | 7c717ba55a0b |
parent 56369 | 2704ca85be98 |
child 56371 | fb9ae0727548 |
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Wed Apr 02 18:35:01 2014 +0200 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Wed Apr 02 18:35:02 2014 +0200 @@ -903,8 +903,6 @@ qed qed - - subsection {* Differentiability of inverse function (most basic form) *} lemma has_derivative_inverse_basic: