src/HOL/Import/HOL/bword_num.imp
changeset 14516 a183dec876ab
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Import/HOL/bword_num.imp	Fri Apr 02 17:37:45 2004 +0200
     1.3 @@ -0,0 +1,58 @@
     1.4 +import
     1.5 +
     1.6 +import_segment "hol4"
     1.7 +
     1.8 +def_maps
     1.9 +  "VB" > "VB_def"
    1.10 +  "NBWORD" > "NBWORD_def"
    1.11 +  "BV" > "BV_def"
    1.12 +  "BNVAL" > "BNVAL_def"
    1.13 +
    1.14 +const_maps
    1.15 +  "VB" > "HOL4Vec.bword_num.VB"
    1.16 +  "NBWORD" > "HOL4Vec.bword_num.NBWORD"
    1.17 +  "BV" > "HOL4Vec.bword_num.BV"
    1.18 +
    1.19 +thm_maps
    1.20 +  "ZERO_WORD_VAL" > "HOL4Vec.bword_num.ZERO_WORD_VAL"
    1.21 +  "WSPLIT_NBWORD_0" > "HOL4Vec.bword_num.WSPLIT_NBWORD_0"
    1.22 +  "WSEG_NBWORD_SUC" > "HOL4Vec.bword_num.WSEG_NBWORD_SUC"
    1.23 +  "WSEG_NBWORD" > "HOL4Vec.bword_num.WSEG_NBWORD"
    1.24 +  "WORDLEN_NBWORD" > "HOL4Vec.bword_num.WORDLEN_NBWORD"
    1.25 +  "WCAT_NBWORD_0" > "HOL4Vec.bword_num.WCAT_NBWORD_0"
    1.26 +  "VB_def" > "HOL4Vec.bword_num.VB_def"
    1.27 +  "VB_DEF" > "HOL4Vec.bword_num.VB_DEF"
    1.28 +  "VB_BV" > "HOL4Vec.bword_num.VB_BV"
    1.29 +  "PWORDLEN_NBWORD" > "HOL4Vec.bword_num.PWORDLEN_NBWORD"
    1.30 +  "NBWORD_def" > "HOL4Vec.bword_num.NBWORD_def"
    1.31 +  "NBWORD_SUC_WSEG" > "HOL4Vec.bword_num.NBWORD_SUC_WSEG"
    1.32 +  "NBWORD_SUC_FST" > "HOL4Vec.bword_num.NBWORD_SUC_FST"
    1.33 +  "NBWORD_SUC" > "HOL4Vec.bword_num.NBWORD_SUC"
    1.34 +  "NBWORD_SPLIT" > "HOL4Vec.bword_num.NBWORD_SPLIT"
    1.35 +  "NBWORD_MOD" > "HOL4Vec.bword_num.NBWORD_MOD"
    1.36 +  "NBWORD_DEF" > "HOL4Vec.bword_num.NBWORD_DEF"
    1.37 +  "NBWORD_BNVAL" > "HOL4Vec.bword_num.NBWORD_BNVAL"
    1.38 +  "NBWORD0" > "HOL4Vec.bword_num.NBWORD0"
    1.39 +  "MSB_NBWORD" > "HOL4Vec.bword_num.MSB_NBWORD"
    1.40 +  "EQ_NBWORD0_SPLIT" > "HOL4Vec.bword_num.EQ_NBWORD0_SPLIT"
    1.41 +  "DOUBL_EQ_SHL" > "HOL4Vec.bword_num.DOUBL_EQ_SHL"
    1.42 +  "BV_def" > "HOL4Vec.bword_num.BV_def"
    1.43 +  "BV_VB" > "HOL4Vec.bword_num.BV_VB"
    1.44 +  "BV_LESS_2" > "HOL4Vec.bword_num.BV_LESS_2"
    1.45 +  "BV_DEF" > "HOL4Vec.bword_num.BV_DEF"
    1.46 +  "BNVAL_WCAT2" > "HOL4Vec.bword_num.BNVAL_WCAT2"
    1.47 +  "BNVAL_WCAT1" > "HOL4Vec.bword_num.BNVAL_WCAT1"
    1.48 +  "BNVAL_WCAT" > "HOL4Vec.bword_num.BNVAL_WCAT"
    1.49 +  "BNVAL_ONTO" > "HOL4Vec.bword_num.BNVAL_ONTO"
    1.50 +  "BNVAL_NVAL" > "HOL4Vec.bword_num.BNVAL_NVAL"
    1.51 +  "BNVAL_NBWORD" > "HOL4Vec.bword_num.BNVAL_NBWORD"
    1.52 +  "BNVAL_MAX" > "HOL4Vec.bword_num.BNVAL_MAX"
    1.53 +  "BNVAL_DEF" > "HOL4Vec.bword_num.BNVAL_DEF"
    1.54 +  "BNVAL_11" > "HOL4Vec.bword_num.BNVAL_11"
    1.55 +  "BNVAL0" > "HOL4Vec.bword_num.BNVAL0"
    1.56 +  "BIT_NBWORD0" > "HOL4Vec.bword_num.BIT_NBWORD0"
    1.57 +  "ADD_BNVAL_SPLIT" > "HOL4Vec.bword_num.ADD_BNVAL_SPLIT"
    1.58 +  "ADD_BNVAL_RIGHT" > "HOL4Vec.bword_num.ADD_BNVAL_RIGHT"
    1.59 +  "ADD_BNVAL_LEFT" > "HOL4Vec.bword_num.ADD_BNVAL_LEFT"
    1.60 +
    1.61 +end