load main entry points sequentially, for reduced memory demands;
authorwenzelm
Sun Jan 11 17:34:02 2009 +0100 (2009-01-11)
changeset 29447a5d0c3cf305f
parent 29446 46d5b9f73791
child 29448 34b9652b2f45
load main entry points sequentially, for reduced memory demands;
src/HOL/ROOT.ML
     1.1 --- a/src/HOL/ROOT.ML	Sun Jan 11 16:56:59 2009 +0100
     1.2 +++ b/src/HOL/ROOT.ML	Sun Jan 11 17:34:02 2009 +0100
     1.3 @@ -1,5 +1,6 @@
     1.4  (* Classical Higher-order Logic -- batteries included *)
     1.5  
     1.6 +use_thy "Main";
     1.7  use_thy "Complex_Main";
     1.8  
     1.9  val HOL_proofs = ! Proofterm.proofs;