src/HOL/Import/HOL/word_bitop.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   "WMAP" > "WMAP_def"
     7   "SHR" > "SHR_def"
     8   "SHL" > "SHL_def"
     9   "PBITOP" > "PBITOP_primdef"
    10   "PBITBOP" > "PBITBOP_primdef"
    11   "FORALLBITS" > "FORALLBITS_def"
    12   "EXISTSABIT" > "EXISTSABIT_def"
    13 
    14 const_maps
    15   "SHR" > "HOL4Vec.word_bitop.SHR"
    16   "SHL" > "HOL4Vec.word_bitop.SHL"
    17   "PBITOP" > "HOL4Vec.word_bitop.PBITOP"
    18   "PBITBOP" > "HOL4Vec.word_bitop.PBITBOP"
    19 
    20 thm_maps
    21   "WSEG_SHL_0" > "HOL4Vec.word_bitop.WSEG_SHL_0"
    22   "WSEG_SHL" > "HOL4Vec.word_bitop.WSEG_SHL"
    23   "WMAP_o" > "HOL4Vec.word_bitop.WMAP_o"
    24   "WMAP_WSEG" > "HOL4Vec.word_bitop.WMAP_WSEG"
    25   "WMAP_WCAT" > "HOL4Vec.word_bitop.WMAP_WCAT"
    26   "WMAP_PWORDLEN" > "HOL4Vec.word_bitop.WMAP_PWORDLEN"
    27   "WMAP_PBITOP" > "HOL4Vec.word_bitop.WMAP_PBITOP"
    28   "WMAP_DEF" > "HOL4Vec.word_bitop.WMAP_DEF"
    29   "WMAP_BIT" > "HOL4Vec.word_bitop.WMAP_BIT"
    30   "WMAP_0" > "HOL4Vec.word_bitop.WMAP_0"
    31   "SHR_def" > "HOL4Vec.word_bitop.SHR_def"
    32   "SHR_WSEG_NF" > "HOL4Vec.word_bitop.SHR_WSEG_NF"
    33   "SHR_WSEG_1F" > "HOL4Vec.word_bitop.SHR_WSEG_1F"
    34   "SHR_WSEG" > "HOL4Vec.word_bitop.SHR_WSEG"
    35   "SHR_DEF" > "HOL4Vec.word_bitop.SHR_DEF"
    36   "SHL_def" > "HOL4Vec.word_bitop.SHL_def"
    37   "SHL_WSEG_NF" > "HOL4Vec.word_bitop.SHL_WSEG_NF"
    38   "SHL_WSEG_1F" > "HOL4Vec.word_bitop.SHL_WSEG_1F"
    39   "SHL_WSEG" > "HOL4Vec.word_bitop.SHL_WSEG"
    40   "SHL_DEF" > "HOL4Vec.word_bitop.SHL_DEF"
    41   "PBITOP_primdef" > "HOL4Vec.word_bitop.PBITOP_primdef"
    42   "PBITOP_def" > "HOL4Vec.word_bitop.PBITOP_def"
    43   "PBITOP_WSEG" > "HOL4Vec.word_bitop.PBITOP_WSEG"
    44   "PBITOP_PWORDLEN" > "HOL4Vec.word_bitop.PBITOP_PWORDLEN"
    45   "PBITOP_BIT" > "HOL4Vec.word_bitop.PBITOP_BIT"
    46   "PBITBOP_primdef" > "HOL4Vec.word_bitop.PBITBOP_primdef"
    47   "PBITBOP_def" > "HOL4Vec.word_bitop.PBITBOP_def"
    48   "PBITBOP_WSEG" > "HOL4Vec.word_bitop.PBITBOP_WSEG"
    49   "PBITBOP_PWORDLEN" > "HOL4Vec.word_bitop.PBITBOP_PWORDLEN"
    50   "PBITBOP_EXISTS" > "HOL4Vec.word_bitop.PBITBOP_EXISTS"
    51   "NOT_FORALLBITS" > "HOL4Vec.word_bitop.NOT_FORALLBITS"
    52   "NOT_EXISTSABIT" > "HOL4Vec.word_bitop.NOT_EXISTSABIT"
    53   "IN_PBITOP" > "HOL4Vec.word_bitop.IN_PBITOP"
    54   "IN_PBITBOP" > "HOL4Vec.word_bitop.IN_PBITBOP"
    55   "FORALLBITS_WSEG" > "HOL4Vec.word_bitop.FORALLBITS_WSEG"
    56   "FORALLBITS_WCAT" > "HOL4Vec.word_bitop.FORALLBITS_WCAT"
    57   "FORALLBITS_DEF" > "HOL4Vec.word_bitop.FORALLBITS_DEF"
    58   "FORALLBITS" > "HOL4Vec.word_bitop.FORALLBITS"
    59   "EXISTSABIT_WSEG" > "HOL4Vec.word_bitop.EXISTSABIT_WSEG"
    60   "EXISTSABIT_WCAT" > "HOL4Vec.word_bitop.EXISTSABIT_WCAT"
    61   "EXISTSABIT_DEF" > "HOL4Vec.word_bitop.EXISTSABIT_DEF"
    62   "EXISTSABIT" > "HOL4Vec.word_bitop.EXISTSABIT"
    63 
    64 end