| changeset 29304 | 5c71a6da989d |
| parent 29249 | 4dc278c8dc59 |
| child 29447 | a5d0c3cf305f |
| 29303:57f0d287375e | 29304:5c71a6da989d |
|---|---|
1 (* Title: HOL/ROOT.ML |
1 (* Classical Higher-order Logic -- batteries included *) |
2 |
|
3 Classical Higher-order Logic -- batteries included. |
|
4 *) |
|
5 |
2 |
6 use_thy "Complex_Main"; |
3 use_thy "Complex_Main"; |
7 |
4 |
8 val HOL_proofs = ! Proofterm.proofs; |
5 val HOL_proofs = ! Proofterm.proofs; |
9 |