changeset 39941 | 02fcd9cd1eac |
parent 38393 | 7c045c03598f |
child 39946 | 78faa9b31202 |
39940:1f01c9b2b76b | 39941:02fcd9cd1eac |
---|---|
1 header {* Plain HOL *} |
1 header {* Plain HOL *} |
2 |
2 |
3 theory Plain |
3 theory Plain |
4 imports Datatype FunDef Extraction |
4 imports Datatype FunDef Extraction Meson |
5 begin |
5 begin |
6 |
6 |
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}. |