src/HOL/Complex_Main.thy

move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings

header {* Comprehensive Complex Theory *}

theory Complex_Main
imports
  Main
  Real
  Complex
  Log
  Ln
  Taylor
  Deriv
begin

end