| changeset 33296 | a3924d1069e5 |
| parent 30327 | 4d1185c77f4a |
| child 33593 | ef54e2108b74 |
| 33275:b497b2574bf6 | 33296:a3924d1069e5 |
|---|---|
1 header {* Plain HOL *} |
1 header {* Plain HOL *} |
2 |
2 |
3 theory Plain |
3 theory Plain |
4 imports Datatype FunDef Record Extraction Divides |
4 imports Datatype FunDef Record Extraction |
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}. |