changeset 30126 | 332e739b6b0e |
parent 29638 | 1f8f3d26a2cf |
child 33113 | 0f6e30b87cf1 |
child 33615 | 261abc2e3155 |
30124:b956bf0dc87c | 30126:332e739b6b0e |
---|---|
1 (* Classical Higher-order Logic -- batteries included *) |
1 (* Classical Higher-order Logic -- batteries included *) |
2 |
2 |
3 use_thy "Main"; |
|
4 share_common_data (); |
|
5 use_thy "Complex_Main"; |
3 use_thy "Complex_Main"; |
6 |
4 |
7 val HOL_proofs = ! Proofterm.proofs; |
5 val HOL_proofs = ! Proofterm.proofs; |