src/HOL/Import/HOL/num.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 17188 a26a4fc323ed
child 37387 3581483cca6c
permissions -rw-r--r--
adaptions to codegen_package
     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"
    15   "INDUCTION" > "List.lexn.induct"
    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