src/HOL/ROOT.ML

added "no_assms" option to Refute, and include structured proof assumptions by default;
will do the same for Quickcheck unless there are objections

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

use_thys ["Complex_Main"];

val HOL_proofs = ! Proofterm.proofs;