src/HOL/ROOT.ML

proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;

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

use_thy "Complex_Main";

val HOL_proofs = ! Proofterm.proofs;