src/HOL/Import/HOL/bword_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   "WXOR" > "WXOR_def"
     7   "WOR" > "WOR_def"
     8   "WNOT" > "WNOT_def"
     9   "WAND" > "WAND_def"
    10 
    11 thm_maps
    12   "WXOR_DEF" > "HOL4Vec.bword_bitop.WXOR_DEF"
    13   "WOR_DEF" > "HOL4Vec.bword_bitop.WOR_DEF"
    14   "WNOT_WNOT" > "HOL4Vec.bword_bitop.WNOT_WNOT"
    15   "WNOT_DEF" > "HOL4Vec.bword_bitop.WNOT_DEF"
    16   "WCAT_WNOT" > "HOL4Vec.bword_bitop.WCAT_WNOT"
    17   "WAND_DEF" > "HOL4Vec.bword_bitop.WAND_DEF"
    18   "PBITOP_WNOT" > "HOL4Vec.bword_bitop.PBITOP_WNOT"
    19   "PBITBOP_WXOR" > "HOL4Vec.bword_bitop.PBITBOP_WXOR"
    20   "PBITBOP_WOR" > "HOL4Vec.bword_bitop.PBITBOP_WOR"
    21   "PBITBOP_WAND" > "HOL4Vec.bword_bitop.PBITBOP_WAND"
    22 
    23 end