src/HOL/Import/HOL/word_num.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   "NWORD" > "NWORD_def"
     7   "NVAL" > "NVAL_def"
     8   "NLIST" > "NLIST_def"
     9   "LVAL" > "LVAL_def"
    10 
    11 const_maps
    12   "NWORD" > "HOL4Vec.word_num.NWORD"
    13   "LVAL" > "HOL4Vec.word_num.LVAL"
    14 
    15 thm_maps
    16   "NWORD_def" > "HOL4Vec.word_num.NWORD_def"
    17   "NWORD_PWORDLEN" > "HOL4Vec.word_num.NWORD_PWORDLEN"
    18   "NWORD_LENGTH" > "HOL4Vec.word_num.NWORD_LENGTH"
    19   "NWORD_DEF" > "HOL4Vec.word_num.NWORD_DEF"
    20   "NVAL_WORDLEN_0" > "HOL4Vec.word_num.NVAL_WORDLEN_0"
    21   "NVAL_WCAT2" > "HOL4Vec.word_num.NVAL_WCAT2"
    22   "NVAL_WCAT1" > "HOL4Vec.word_num.NVAL_WCAT1"
    23   "NVAL_WCAT" > "HOL4Vec.word_num.NVAL_WCAT"
    24   "NVAL_MAX" > "HOL4Vec.word_num.NVAL_MAX"
    25   "NVAL_DEF" > "HOL4Vec.word_num.NVAL_DEF"
    26   "NVAL1" > "HOL4Vec.word_num.NVAL1"
    27   "NVAL0" > "HOL4Vec.word_num.NVAL0"
    28   "NLIST_DEF" > "HOL4Vec.word_num.NLIST_DEF"
    29   "LVAL_def" > "HOL4Vec.word_num.LVAL_def"
    30   "LVAL_SNOC" > "HOL4Vec.word_num.LVAL_SNOC"
    31   "LVAL_MAX" > "HOL4Vec.word_num.LVAL_MAX"
    32   "LVAL_DEF" > "HOL4Vec.word_num.LVAL_DEF"
    33   "LVAL" > "HOL4Vec.word_num.LVAL"
    34 
    35 end