author | wenzelm |
Mon, 16 Mar 2009 18:24:30 +0100 | |
changeset 30549 | d2d7874648bd |
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 |