changeset 29447 | a5d0c3cf305f |
parent 29304 | 5c71a6da989d |
child 29638 | 1f8f3d26a2cf |
29446:46d5b9f73791 | 29447:a5d0c3cf305f |
---|---|
1 (* Classical Higher-order Logic -- batteries included *) |
1 (* Classical Higher-order Logic -- batteries included *) |
2 |
2 |
3 use_thy "Main"; |
|
3 use_thy "Complex_Main"; |
4 use_thy "Complex_Main"; |
4 |
5 |
5 val HOL_proofs = ! Proofterm.proofs; |
6 val HOL_proofs = ! Proofterm.proofs; |