src/HOL/Complex_Main.thy

if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem

header {* Comprehensive Complex Theory *}

theory Complex_Main
imports
  Main
  Real
  SupInf
  Complex
  Log
  Ln
  Taylor
  Deriv
begin

end