| changeset 16417 | 9bc16273c2d4 |
| parent 15647 | b1f486a9c56b |
| child 17566 | 484ff733f29c |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
1 (* Title: HOL/Import/Generate-HOL/GenHOL4Real.thy |
1 (* Title: HOL/Import/Generate-HOL/GenHOL4Real.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 GenHOL4Real = GenHOL4Base: |
6 theory GenHOL4Real imports GenHOL4Base begin |
7 |
7 |
8 import_segment "hol4"; |
8 import_segment "hol4"; |
9 |
9 |
10 setup_dump "../HOL" "HOL4Real"; |
10 setup_dump "../HOL" "HOL4Real"; |
11 |
11 |