src/HOL/ROOT.ML

--- a/src/HOL/ROOT.ML	Wed Sep 17 21:27:08 2008 +0200
+++ b/src/HOL/ROOT.ML	Wed Sep 17 21:27:14 2008 +0200
@@ -5,3 +5,6 @@
 *)
 
 use_thy "Complex/Complex_Main";
+
+val HOL_proofs = ! Proofterm.proofs;
+