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/combin.imp
author wenzelm
Mon, 09 Oct 2006 02:20:01 +0200
changeset 20907 9673c67dde9b
parent 14516 a183dec876ab
child 44763 b50d5d694838
permissions -rw-r--r--
lemmas/theorems/declare: Specification.theorems;

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.o_apply"
  "o_DEF" > "Fun.o_apply"
  "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