| changeset 16417 | 9bc16273c2d4 |
| parent 14620 | 1be590fd2422 |
| child 17566 | 484ff733f29c |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
1 (* Title: HOL/Import/Generate-HOL/GenHOL4Vec.thy |
1 (* Title: HOL/Import/Generate-HOL/GenHOL4Vec.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Sebastian Skalberg (TU Muenchen) |
3 Author: Sebastian Skalberg (TU Muenchen) |
4 *) |
4 *) |
5 |
5 |
6 theory GenHOL4Vec = GenHOL4Base: |
6 theory GenHOL4Vec imports GenHOL4Base begin |
7 |
7 |
8 import_segment "hol4"; |
8 import_segment "hol4"; |
9 |
9 |
10 setup_dump "../HOL" "HOL4Vec"; |
10 setup_dump "../HOL" "HOL4Vec"; |
11 |
11 |