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
skalberg@14516
     1
import
skalberg@14516
     2
skalberg@14516
     3
import_segment "hol4"
skalberg@14516
     4
skalberg@14516
     5
def_maps
skalberg@14516
     6
  "ICARRY" > "ICARRY_def"
skalberg@14516
     7
  "ACARRY" > "ACARRY_def"
skalberg@14516
     8
skalberg@14516
     9
thm_maps
skalberg@14516
    10
  "WSEG_NBWORD_ADD" > "HOL4Vec.bword_arith.WSEG_NBWORD_ADD"
skalberg@14516
    11
  "ICARRY_WSEG" > "HOL4Vec.bword_arith.ICARRY_WSEG"
skalberg@14516
    12
  "ICARRY_DEF" > "HOL4Vec.bword_arith.ICARRY_DEF"
skalberg@14516
    13
  "BNVAL_LESS_EQ" > "HOL4Vec.bword_arith.BNVAL_LESS_EQ"
skalberg@14516
    14
  "ADD_WORD_SPLIT" > "HOL4Vec.bword_arith.ADD_WORD_SPLIT"
skalberg@14516
    15
  "ADD_NBWORD_EQ0_SPLIT" > "HOL4Vec.bword_arith.ADD_NBWORD_EQ0_SPLIT"
skalberg@14516
    16
  "ADD_BV_BNVAL_LESS_EQ1" > "HOL4Vec.bword_arith.ADD_BV_BNVAL_LESS_EQ1"
skalberg@14516
    17
  "ADD_BV_BNVAL_LESS_EQ" > "HOL4Vec.bword_arith.ADD_BV_BNVAL_LESS_EQ"
skalberg@14516
    18
  "ADD_BV_BNVAL_DIV_LESS_EQ1" > "HOL4Vec.bword_arith.ADD_BV_BNVAL_DIV_LESS_EQ1"
skalberg@14516
    19
  "ADD_BNVAL_LESS_EQ1" > "HOL4Vec.bword_arith.ADD_BNVAL_LESS_EQ1"
skalberg@14516
    20
  "ACARRY_WSEG" > "HOL4Vec.bword_arith.ACARRY_WSEG"
skalberg@14516
    21
  "ACARRY_MSB" > "HOL4Vec.bword_arith.ACARRY_MSB"
skalberg@14516
    22
  "ACARRY_EQ_ICARRY" > "HOL4Vec.bword_arith.ACARRY_EQ_ICARRY"
skalberg@14516
    23
  "ACARRY_EQ_ADD_DIV" > "HOL4Vec.bword_arith.ACARRY_EQ_ADD_DIV"
skalberg@14516
    24
  "ACARRY_DEF" > "HOL4Vec.bword_arith.ACARRY_DEF"
skalberg@14516
    25
  "ACARRY_ACARRY_WSEG" > "HOL4Vec.bword_arith.ACARRY_ACARRY_WSEG"
skalberg@14516
    26
skalberg@14516
    27
end