src/HOL/Import/HOL/bword_arith.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 14516 a183dec876ab
permissions -rw-r--r--
adaptions to codegen_package
     1 import
     2 
     3 import_segment "hol4"
     4 
     5 def_maps
     6   "ICARRY" > "ICARRY_def"
     7   "ACARRY" > "ACARRY_def"
     8 
     9 thm_maps
    10   "WSEG_NBWORD_ADD" > "HOL4Vec.bword_arith.WSEG_NBWORD_ADD"
    11   "ICARRY_WSEG" > "HOL4Vec.bword_arith.ICARRY_WSEG"
    12   "ICARRY_DEF" > "HOL4Vec.bword_arith.ICARRY_DEF"
    13   "BNVAL_LESS_EQ" > "HOL4Vec.bword_arith.BNVAL_LESS_EQ"
    14   "ADD_WORD_SPLIT" > "HOL4Vec.bword_arith.ADD_WORD_SPLIT"
    15   "ADD_NBWORD_EQ0_SPLIT" > "HOL4Vec.bword_arith.ADD_NBWORD_EQ0_SPLIT"
    16   "ADD_BV_BNVAL_LESS_EQ1" > "HOL4Vec.bword_arith.ADD_BV_BNVAL_LESS_EQ1"
    17   "ADD_BV_BNVAL_LESS_EQ" > "HOL4Vec.bword_arith.ADD_BV_BNVAL_LESS_EQ"
    18   "ADD_BV_BNVAL_DIV_LESS_EQ1" > "HOL4Vec.bword_arith.ADD_BV_BNVAL_DIV_LESS_EQ1"
    19   "ADD_BNVAL_LESS_EQ1" > "HOL4Vec.bword_arith.ADD_BNVAL_LESS_EQ1"
    20   "ACARRY_WSEG" > "HOL4Vec.bword_arith.ACARRY_WSEG"
    21   "ACARRY_MSB" > "HOL4Vec.bword_arith.ACARRY_MSB"
    22   "ACARRY_EQ_ICARRY" > "HOL4Vec.bword_arith.ACARRY_EQ_ICARRY"
    23   "ACARRY_EQ_ADD_DIV" > "HOL4Vec.bword_arith.ACARRY_EQ_ADD_DIV"
    24   "ACARRY_DEF" > "HOL4Vec.bword_arith.ACARRY_DEF"
    25   "ACARRY_ACARRY_WSEG" > "HOL4Vec.bword_arith.ACARRY_ACARRY_WSEG"
    26 
    27 end