--- a/src/HOL/Analysis/Derivative.thy Sat Nov 02 20:52:24 2019 +0000
+++ b/src/HOL/Analysis/Derivative.thy Sat Nov 02 21:42:45 2019 +0000
@@ -7,7 +7,8 @@
theory Derivative
imports
- Starlike
+ Convex_Euclidean_Space
+ Abstract_Limits
Operator_Norm
Uniform_Limit
Bounded_Linear_Function