| changeset 17566 | 484ff733f29c |
| parent 16417 | 9bc16273c2d4 |
| child 41589 | bbd861837ebc |
| 17565:7322f37d3344 | 17566:484ff733f29c |
|---|---|
7 |
7 |
8 import_segment "hol4"; |
8 import_segment "hol4"; |
9 |
9 |
10 setup_dump "../HOL" "HOL4Vec"; |
10 setup_dump "../HOL" "HOL4Vec"; |
11 |
11 |
12 append_dump "theory HOL4Vec = HOL4Base:"; |
12 append_dump "theory HOL4Vec imports HOL4Base begin"; |
13 |
13 |
14 import_theory res_quan; |
14 import_theory res_quan; |
15 end_import; |
15 end_import; |
16 |
16 |
17 import_theory word_base; |
17 import_theory word_base; |