--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Wed Sep 04 14:16:27 2019 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Wed Sep 04 15:27:04 2019 +0100
@@ -3,7 +3,7 @@
text\<open>By John Harrison et al. Ported from HOL Light by L C Paulson (2015)\<close>
theory Cauchy_Integral_Theorem
-imports Complex_Transcendental Henstock_Kurzweil_Integration Weierstrass_Theorems Ordered_Euclidean_Space
+imports Complex_Transcendental Henstock_Kurzweil_Integration Weierstrass_Theorems Retracts
begin
lemma leibniz_rule_holomorphic: