src/HOL/Import/HOL/sum.imp
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Wed, 07 Sep 2011 07:59:45 +0900
changeset 44763 b50d5d694838
parent 15647 b1f486a9c56b
permissions -rw-r--r--
HOL/Import: Update HOL4 generated files to current Isabelle.

import

import_segment "hol4"

type_maps
  "sum" > "Sum_Type.sum"

const_maps
  "sum_case" > "Sum_Type.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" > "Sum_Type.Inr_not_Inl"
  "sum_distinct" > "Sum_Type.Inl_not_Inr"
  "sum_case_def" > "HOL4Compat.sum_case_def"
  "sum_case_cong" > "HOL4Base.sum.sum_case_cong"
  "sum_axiom" > "HOL4Compat.sum_axiom"
  "sum_INDUCT" > "Sum_Type.sum.induct"
  "sum_CASES" > "Sum_Type.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" > "Sum_Type.Inr_not_Inl"
  "INR_INL_11" > "HOL4Compat.INR_INL_11"
  "INR" > "HOL4Base.sum.INR"
  "INL" > "HOL4Base.sum.INL"

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

end