1
(* Classical Higher-order Logic -- batteries included *)
2
3
use_thy "Complex_Main";
4
5
val HOL_proofs = ! Proofterm.proofs;