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