src/HOL/ROOT.ML

added command 'ProofGeneral.pr' for PG 4.0;

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

use_thys ["Complex_Main"];

val HOL_proofs = ! Proofterm.proofs;