| changeset 29820 | 07f53494cf20 |
| parent 29609 | a010aab5bed0 |
| child 29837 | eb7e62c0f53c |
| 29802:d201a838d0f7 | 29820:07f53494cf20 |
|---|---|
1 header {* Plain HOL *} |
1 header {* Plain HOL *} |
2 |
2 |
3 theory Plain |
3 theory Plain |
4 imports Datatype FunDef Record SAT Extraction Divides |
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}. |