src/HOL/ROOT.ML

added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal)

(* Classical Higher-order Logic -- batteries included *)

use_thys ["Complex_Main"];