src/HOL/Complex_Main.thy

remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)

header {* Comprehensive Complex Theory *}

theory Complex_Main
imports
  Main
  Real
  Complex
  Transcendental
  Taylor
  Deriv
begin

end