--- a/src/HOL/ROOT.ML Sun Jan 11 16:56:59 2009 +0100 +++ b/src/HOL/ROOT.ML Sun Jan 11 17:34:02 2009 +0100 @@ -1,5 +1,6 @@ (* Classical Higher-order Logic -- batteries included *) +use_thy "Main"; use_thy "Complex_Main"; val HOL_proofs = ! Proofterm.proofs;