# HG changeset patch
# User wenzelm
# Date 1231691642 -3600
# Node ID a5d0c3cf305fe762856c848cfcce0c0ae10dfeeb
# Parent  46d5b9f737917da7b9b0add372dd183ea96907d5
load main entry points sequentially, for reduced memory demands;

diff -r 46d5b9f73791 -r a5d0c3cf305f src/HOL/ROOT.ML
--- 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;