| author | wenzelm |
| Thu, 27 May 2010 18:10:37 +0200 | |
| changeset 37146 | f652333bbf8e |
| parent 17188 | a26a4fc323ed |
| child 37387 | 3581483cca6c |
| permissions | -rw-r--r-- |
| 14516 | 1 |
import |
2 |
||
3 |
import_segment "hol4" |
|
4 |
||
5 |
type_maps |
|
6 |
"num" > "nat" |
|
7 |
||
8 |
const_maps |
|
9 |
"SUC" > "Suc" |
|
10 |
"0" > "0" :: "nat" |
|
11 |
||
12 |
thm_maps |
|
13 |
"NOT_SUC" > "Nat.nat.simps_1" |
|
14 |
"INV_SUC" > "Nat.Suc_inject" |
|
| 17188 | 15 |
"INDUCTION" > "List.lexn.induct" |
| 14516 | 16 |
|
17 |
ignore_thms |
|
18 |
"num_TY_DEF" |
|
19 |
"num_ISO_DEF" |
|
20 |
"ZERO_REP_DEF" |
|
21 |
"ZERO_DEF" |
|
22 |
"SUC_REP_DEF" |
|
23 |
"SUC_DEF" |
|
24 |
"IS_NUM_REP" |
|
25 |
||
26 |
end |