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 *)