| changeset 27367 | a75d71c73362 |
| parent 26729 | 43a72d892594 |
| child 28091 | 50f2d6ba024c |
| 27366:d0cda1ea705e | 27367:a75d71c73362 |
|---|---|
3 *) |
3 *) |
4 |
4 |
5 header {* Main HOL *} |
5 header {* Main HOL *} |
6 |
6 |
7 theory Main |
7 theory Main |
8 imports Map |
8 imports Plain Map Presburger Recdef |
9 begin |
9 begin |
10 |
10 |
11 ML {* val HOL_proofs = ! Proofterm.proofs *} |
11 ML {* val HOL_proofs = ! Proofterm.proofs *} |
12 |
12 |
13 ML {* path_add "~~/src/HOL/Library" *} |
13 text {* See further \cite{Nipkow-et-al:2002:tutorial} *} |
14 |
14 |
15 end |
15 end |