changeset 30073 | a4ad0c08b7d9 |
parent 29837 | eb7e62c0f53c |
child 30327 | 4d1185c77f4a |
30072:4eecd8b9b6cf | 30073:a4ad0c08b7d9 |
---|---|
1 header {* Plain HOL *} |
1 header {* Plain HOL *} |
2 |
2 |
3 theory Plain |
3 theory Plain |
4 imports Datatype FunDef Record Extraction Divides Fact |
4 imports Datatype FunDef Record Extraction Divides |
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}. |