src/HOL/Analysis/Lipschitz.thy

--- a/src/HOL/Analysis/Lipschitz.thy	Tue Aug 27 22:31:21 2019 +0200
+++ b/src/HOL/Analysis/Lipschitz.thy	Tue Aug 27 22:41:47 2019 +0200
@@ -5,7 +5,8 @@
 section \<open>Lipschitz Continuity\<close>
 
 theory Lipschitz
-imports Borel_Space
+  imports
+    Derivative
 begin
 
 definition\<^marker>\<open>tag important\<close> lipschitz_on