Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Import/HOL/num.imp
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Wed, 07 Sep 2011 07:59:45 +0900
changeset 44763 b50d5d694838
parent 37387 3581483cca6c
permissions -rw-r--r--
HOL/Import: Update HOL4 generated files to current Isabelle.

import

import_segment "hol4"

type_maps
  "num" > "Nat.nat"

const_maps
  "SUC" > "Nat.Suc"
  "0" > "Groups.zero_class.zero" :: "nat"

thm_maps
  "NOT_SUC" > "Nat.Suc_not_Zero"
  "INV_SUC" > "Nat.Suc_inject"
  "INDUCTION" > "Fact.fact_nat.induct"

ignore_thms
  "num_TY_DEF"
  "num_ISO_DEF"
  "ZERO_REP_DEF"
  "ZERO_DEF"
  "SUC_REP_DEF"
  "SUC_DEF"
  "IS_NUM_REP"

end
isabelle