--- a/src/HOL/ROOT.ML Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/ROOT.ML Sat Oct 24 16:55:42 2009 +0200
@@ -1,5 +1,6 @@
(* Classical Higher-order Logic -- batteries included *)
+Toplevel.debug := true;
use_thy "Complex_Main";
val HOL_proofs = ! Proofterm.proofs;