(* Classical Higher-order Logic -- batteries included *) use_thys ["Complex_Main"]; val HOL_proofs = ! Proofterm.proofs;