author | huffman |
Mon, 23 Feb 2009 16:25:52 -0800 | |
changeset 30079 | 293b896b9c25 |
parent 29638 | 1f8f3d26a2cf |
child 30126 | 332e739b6b0e |
permissions | -rw-r--r-- |
29304 | 1 |
(* Classical Higher-order Logic -- batteries included *) |
923 | 2 |
|
29447
a5d0c3cf305f
load main entry points sequentially, for reduced memory demands;
wenzelm
parents:
29304
diff
changeset
|
3 |
use_thy "Main"; |
29638
1f8f3d26a2cf
added share_common_data -- reduces heap space, but takes long;
wenzelm
parents:
29447
diff
changeset
|
4 |
share_common_data (); |
29005 | 5 |
use_thy "Complex_Main"; |
28263 | 6 |
|
7 |
val HOL_proofs = ! Proofterm.proofs; |