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