src/HOL/Import/HOL/num.imp
author obua
Mon Aug 29 16:51:39 2005 +0200 (2005-08-29)
changeset 17188 a26a4fc323ed
parent 15647 b1f486a9c56b
child 37387 3581483cca6c
permissions -rw-r--r--
Updated import.
skalberg@14516
     1
import
skalberg@14516
     2
skalberg@14516
     3
import_segment "hol4"
skalberg@14516
     4
skalberg@14516
     5
type_maps
skalberg@14516
     6
  "num" > "nat"
skalberg@14516
     7
skalberg@14516
     8
const_maps
skalberg@14516
     9
  "SUC" > "Suc"
skalberg@14516
    10
  "0" > "0" :: "nat"
skalberg@14516
    11
skalberg@14516
    12
thm_maps
skalberg@14516
    13
  "NOT_SUC" > "Nat.nat.simps_1"
skalberg@14516
    14
  "INV_SUC" > "Nat.Suc_inject"
obua@17188
    15
  "INDUCTION" > "List.lexn.induct"
skalberg@14516
    16
skalberg@14516
    17
ignore_thms
skalberg@14516
    18
  "num_TY_DEF"
skalberg@14516
    19
  "num_ISO_DEF"
skalberg@14516
    20
  "ZERO_REP_DEF"
skalberg@14516
    21
  "ZERO_DEF"
skalberg@14516
    22
  "SUC_REP_DEF"
skalberg@14516
    23
  "SUC_DEF"
skalberg@14516
    24
  "IS_NUM_REP"
skalberg@14516
    25
skalberg@14516
    26
end