author | wenzelm |
Thu, 27 May 2010 18:10:37 +0200 | |
changeset 37146 | f652333bbf8e |
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