| changeset 17566 | 484ff733f29c |
| parent 16417 | 9bc16273c2d4 |
| child 17694 | b7870c2bd7df |
| 17565:7322f37d3344 | 17566:484ff733f29c |
|---|---|
7 |
7 |
8 import_segment "hol4"; |
8 import_segment "hol4"; |
9 |
9 |
10 setup_dump "../HOL" "HOL4Real"; |
10 setup_dump "../HOL" "HOL4Real"; |
11 |
11 |
12 append_dump "theory HOL4Real = HOL4Base:"; |
12 append_dump "theory HOL4Real imports HOL4Base begin"; |
13 |
13 |
14 import_theory realax; |
14 import_theory realax; |
15 |
15 |
16 type_maps |
16 type_maps |
17 real > RealDef.real; |
17 real > RealDef.real; |