src/HOL/Import/HOL/combin.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 14516 a183dec876ab
child 44763 b50d5d694838
permissions -rw-r--r--
adaptions to codegen_package
     1 import
     2 
     3 import_segment "hol4"
     4 
     5 def_maps
     6   "W" > "W_def"
     7   "S" > "S_def"
     8   "K" > "K_def"
     9   "I" > "I_def"
    10   "C" > "C_def"
    11 
    12 const_maps
    13   "o" > "Fun.comp"
    14   "W" > "HOL4Base.combin.W"
    15   "S" > "HOL4Base.combin.S"
    16   "K" > "HOL4Base.combin.K"
    17   "I" > "HOL4Base.combin.I"
    18   "C" > "HOL4Base.combin.C"
    19 
    20 thm_maps
    21   "o_THM" > "Fun.o_apply"
    22   "o_DEF" > "Fun.o_apply"
    23   "o_ASSOC" > "Fun.o_assoc"
    24   "W_def" > "HOL4Base.combin.W_def"
    25   "W_THM" > "HOL4Base.combin.W_def"
    26   "W_DEF" > "HOL4Base.combin.W_DEF"
    27   "S_def" > "HOL4Base.combin.S_def"
    28   "S_THM" > "HOL4Base.combin.S_def"
    29   "S_DEF" > "HOL4Base.combin.S_DEF"
    30   "K_def" > "HOL4Base.combin.K_def"
    31   "K_THM" > "HOL4Base.combin.K_def"
    32   "K_DEF" > "HOL4Base.combin.K_DEF"
    33   "I_o_ID" > "HOL4Base.combin.I_o_ID"
    34   "I_def" > "HOL4Base.combin.I_def"
    35   "I_THM" > "HOL4Base.combin.I_THM"
    36   "I_DEF" > "HOL4Base.combin.I_DEF"
    37   "C_def" > "HOL4Base.combin.C_def"
    38   "C_THM" > "HOL4Base.combin.C_def"
    39   "C_DEF" > "HOL4Base.combin.C_DEF"
    40 
    41 end