src/HOL/Analysis/Complex_Analysis_Basics.thy
changeset 70620 f95193669ad7
parent 70196 b7ef9090feed
child 70707 125705f5965f
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Tue Aug 27 23:12:28 2019 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Wed Aug 28 00:08:14 2019 +0200
@@ -5,7 +5,7 @@
 section \<open>Complex Analysis Basics\<close>
 
 theory Complex_Analysis_Basics
-  imports Derivative "HOL-Library.Nonpos_Ints"
+  imports Brouwer_Fixpoint "HOL-Library.Nonpos_Ints"
 begin
 
 (* TODO FIXME: A lot of the things in here have nothing to do with complex analysis *)