changeset 29005 | ce378dcfddab |
parent 28952 | 15a4b2cf8c34 |
child 29233 | ce6d35a0bed6 |
29004:a5a91f387791 | 29005:ce378dcfddab |
---|---|
1 (* Title: HOL/ROOT.ML |
1 (* Title: HOL/ROOT.ML |
2 |
2 |
3 Classical Higher-order Logic -- batteries included. |
3 Classical Higher-order Logic -- batteries included. |
4 *) |
4 *) |
5 |
5 |
6 use_thy "Complex/Complex_Main"; |
6 use_thy "Complex_Main"; |
7 |
7 |
8 val HOL_proofs = ! Proofterm.proofs; |
8 val HOL_proofs = ! Proofterm.proofs; |
9 |
9 |