src/HOL/Import/HOL/num.imp
author haftmann
Tue, 08 Jun 2010 16:37:19 +0200
changeset 37387 3581483cca6c
parent 17188 a26a4fc323ed
child 44763 b50d5d694838
permissions -rw-r--r--
qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications

import

import_segment "hol4"

type_maps
  "num" > "Nat.nat"

const_maps
  "SUC" > "Nat.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