| changeset 41886 | aa8dce9ab8a9 |
| parent 41414 | 00b2b6716ed8 |
| child 46691 | 72d81e789106 |
| 41885:1e081bfb2eaf | 41886:aa8dce9ab8a9 |
|---|---|
7 text {* |
7 text {* |
8 Plain bootstrap of fundamental HOL tools and packages; does not |
8 Plain bootstrap of fundamental HOL tools and packages; does not |
9 include @{text Hilbert_Choice}. |
9 include @{text Hilbert_Choice}. |
10 *} |
10 *} |
11 |
11 |
12 ML {* Thy_Load.legacy_path_add "~~/src/HOL/Library" *} |
|
13 |
|
14 end |
12 end |