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/HOL4/Generated/sum.imp
author boehmes
Tue, 27 Mar 2012 17:11:02 +0200
changeset 47155 ade3fc826af3
parent 46787 3d3d8f8929a7
permissions -rw-r--r--
dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct

import

import_segment "hol4"

type_maps
  "sum" > "Sum_Type.sum"

const_maps
  "sum_case" > "Sum_Type.sum.sum_case"
  "OUTR" > "Compatibility.OUTR"
  "OUTL" > "Compatibility.OUTL"
  "ISR" > "Compatibility.ISR"
  "ISL" > "Compatibility.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" > "Compatibility.sum_case_def"
  "sum_case_cong" > "HOL4Base.sum.sum_case_cong"
  "sum_axiom" > "Compatibility.sum_axiom"
  "sum_INDUCT" > "Sum_Type.sum.induct"
  "sum_CASES" > "Sum_Type.sum.nchotomy"
  "OUTR" > "Compatibility.OUTR"
  "OUTL" > "Compatibility.OUTL"
  "ISR" > "Compatibility.ISR"
  "ISL_OR_ISR" > "HOL4Base.sum.ISL_OR_ISR"
  "ISL" > "Compatibility.ISL"
  "INR_neq_INL" > "Sum_Type.Inr_not_Inl"
  "INR_INL_11" > "Compatibility.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
isabelle