src/HOL/Import/HOL/sum.imp
author skalberg
Fri, 01 Apr 2005 18:59:17 +0200
changeset 15647 b1f486a9c56b
parent 14516 a183dec876ab
child 44763 b50d5d694838
permissions -rw-r--r--
Updated import configuration.

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