| author | huffman |
| Fri, 01 Feb 2008 02:38:41 +0100 | |
| changeset 26029 | 46e84ca065f1 |
| parent 14516 | a183dec876ab |
| permissions | -rw-r--r-- |
| 14516 | 1 |
import |
2 |
||
3 |
import_segment "hol4" |
|
4 |
||
5 |
def_maps |
|
6 |
"prime" > "prime_primdef" |
|
7 |
||
8 |
const_maps |
|
9 |
"prime" > "HOL4Base.prime.prime" |
|
10 |
||
11 |
thm_maps |
|
12 |
"prime_primdef" > "HOL4Base.prime.prime_primdef" |
|
13 |
"prime_def" > "HOL4Base.prime.prime_def" |
|
14 |
"NOT_PRIME_1" > "HOL4Base.prime.NOT_PRIME_1" |
|
15 |
"NOT_PRIME_0" > "HOL4Base.prime.NOT_PRIME_0" |
|
16 |
||
17 |
end |