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/combin.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"

def_maps
  "W" > "W_def"
  "S" > "S_def"
  "K" > "K_def"
  "I" > "I_def"
  "C" > "C_def"

const_maps
  "o" > "Fun.comp"
  "W" > "HOL4Base.combin.W"
  "S" > "HOL4Base.combin.S"
  "K" > "HOL4Base.combin.K"
  "I" > "HOL4Base.combin.I"
  "C" > "HOL4Base.combin.C"

thm_maps
  "o_THM" > "Fun.comp_def"
  "o_DEF" > "Fun.comp_def"
  "o_ASSOC" > "Fun.o_assoc"
  "W_def" > "HOL4Base.combin.W_def"
  "W_THM" > "HOL4Base.combin.W_def"
  "W_DEF" > "HOL4Base.combin.W_DEF"
  "S_def" > "HOL4Base.combin.S_def"
  "S_THM" > "HOL4Base.combin.S_def"
  "S_DEF" > "HOL4Base.combin.S_DEF"
  "K_def" > "HOL4Base.combin.K_def"
  "K_THM" > "HOL4Base.combin.K_def"
  "K_DEF" > "HOL4Base.combin.K_DEF"
  "I_o_ID" > "HOL4Base.combin.I_o_ID"
  "I_def" > "HOL4Base.combin.I_def"
  "I_THM" > "HOL4Base.combin.I_THM"
  "I_DEF" > "HOL4Base.combin.I_DEF"
  "C_def" > "HOL4Base.combin.C_def"
  "C_THM" > "HOL4Base.combin.C_def"
  "C_DEF" > "HOL4Base.combin.C_DEF"

end
isabelle