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/sum.imp
author wenzelm
Thu, 27 May 2010 18:10:37 +0200
changeset 37146 f652333bbf8e
parent 15647 b1f486a9c56b
child 44763 b50d5d694838
permissions -rw-r--r--
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;

import

import_segment "hol4"

type_maps
  "sum" > "+"

const_maps
  "sum_case" > "Datatype.sum.sum_case"
  "OUTR" > "HOL4Compat.OUTR"
  "OUTL" > "HOL4Compat.OUTL"
  "ISR" > "HOL4Compat.ISR"
  "ISL" > "HOL4Compat.ISL"
  "INR" > "Sum_Type.Inr"
  "INL" > "Sum_Type.Inl"

thm_maps
  "sum_distinct1" > "Datatype.sum.simps_2"
  "sum_distinct" > "Datatype.sum.simps_1"
  "sum_case_def" > "HOL4Compat.sum_case_def"
  "sum_case_cong" > "HOL4Base.sum.sum_case_cong"
  "sum_INDUCT" > "HOL4Compat.OUTR.induct"
  "sum_CASES" > "Datatype.sum.nchotomy"
  "OUTR" > "HOL4Compat.OUTR"
  "OUTL" > "HOL4Compat.OUTL"
  "ISR" > "HOL4Compat.ISR"
  "ISL_OR_ISR" > "HOL4Base.sum.ISL_OR_ISR"
  "ISL" > "HOL4Compat.ISL"
  "INR_neq_INL" > "Datatype.sum.simps_2"
  "INR_INL_11" > "HOL4Compat.INR_INL_11"
  "INR" > "HOL4Base.sum.INR"
  "INL" > "HOL4Base.sum.INL"

ignore_thms
  "sum_axiom"
  "sum_TY_DEF"
  "sum_ISO_DEF"
  "sum_Axiom"
  "IS_SUM_REP"
  "INR_DEF"
  "INL_DEF"

end
isabelle