1 header {* Plain HOL *}
2
3 theory Plain
4 imports Datatype FunDef Extraction Metis
5 begin
6
7 text {*
8 Plain bootstrap of fundamental HOL tools and packages; does not
9 include @{text Hilbert_Choice}.
10 *}
11
12 end