author | nipkow |
Sun, 22 Feb 2009 17:25:28 +0100 | |
changeset 30056 | 0a35bee25c20 |
parent 17188 | a26a4fc323ed |
child 37387 | 3581483cca6c |
permissions | -rw-r--r-- |
import import_segment "hol4" type_maps "num" > "nat" const_maps "SUC" > "Suc" "0" > "0" :: "nat" thm_maps "NOT_SUC" > "Nat.nat.simps_1" "INV_SUC" > "Nat.Suc_inject" "INDUCTION" > "List.lexn.induct" ignore_thms "num_TY_DEF" "num_ISO_DEF" "ZERO_REP_DEF" "ZERO_DEF" "SUC_REP_DEF" "SUC_DEF" "IS_NUM_REP" end