changeset 29638 | 1f8f3d26a2cf |
parent 29447 | a5d0c3cf305f |
child 30126 | 332e739b6b0e |
29636:d01bada1df33 | 29638:1f8f3d26a2cf |
---|---|
1 (* Classical Higher-order Logic -- batteries included *) |
1 (* Classical Higher-order Logic -- batteries included *) |
2 |
2 |
3 use_thy "Main"; |
3 use_thy "Main"; |
4 share_common_data (); |
|
4 use_thy "Complex_Main"; |
5 use_thy "Complex_Main"; |
5 |
6 |
6 val HOL_proofs = ! Proofterm.proofs; |
7 val HOL_proofs = ! Proofterm.proofs; |