src/HOL/Import/HOL/bits.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 14516 a183dec876ab
child 44763 b50d5d694838
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
  "bit" > "bit_def"
skalberg@14516
     7
  "TIMES_2EXP" > "TIMES_2EXP_primdef"
skalberg@14516
     8
  "SLICE" > "SLICE_primdef"
skalberg@14516
     9
  "SBIT" > "SBIT_primdef"
skalberg@14516
    10
  "MOD_2EXP" > "MOD_2EXP_primdef"
skalberg@14516
    11
  "LSBn" > "LSBn_primdef"
skalberg@14516
    12
  "DIV_2EXP" > "DIV_2EXP_primdef"
skalberg@14516
    13
  "DIVMOD_2EXP" > "DIVMOD_2EXP_primdef"
skalberg@14516
    14
  "DIV2" > "DIV2_primdef"
skalberg@14516
    15
  "BITWISE" > "BITWISE_primdef"
skalberg@14516
    16
  "BITS" > "BITS_primdef"
skalberg@14516
    17
skalberg@14516
    18
const_maps
skalberg@14516
    19
  "bit" > "HOL4Word32.bits.bit"
skalberg@14516
    20
  "TIMES_2EXP" > "HOL4Word32.bits.TIMES_2EXP"
skalberg@14516
    21
  "SLICE" > "HOL4Word32.bits.SLICE"
skalberg@14516
    22
  "SBIT" > "HOL4Word32.bits.SBIT"
skalberg@14516
    23
  "MOD_2EXP" > "HOL4Word32.bits.MOD_2EXP"
skalberg@14516
    24
  "LSBn" > "HOL4Word32.bits.LSBn"
skalberg@14516
    25
  "DIV_2EXP" > "HOL4Word32.bits.DIV_2EXP"
skalberg@14516
    26
  "DIVMOD_2EXP" > "HOL4Word32.bits.DIVMOD_2EXP"
skalberg@14516
    27
  "DIV2" > "HOL4Word32.bits.DIV2"
skalberg@14516
    28
  "BITS" > "HOL4Word32.bits.BITS"
skalberg@14516
    29
skalberg@14516
    30
const_renames
skalberg@14516
    31
  "BIT" > "bit"
skalberg@14516
    32
skalberg@14516
    33
thm_maps
skalberg@14516
    34
  "bit_def" > "HOL4Word32.bits.bit_def"
skalberg@14516
    35
  "ZERO_LT_TWOEXP" > "HOL4Word32.bits.ZERO_LT_TWOEXP"
skalberg@14516
    36
  "TWOEXP_MONO2" > "HOL4Word32.bits.TWOEXP_MONO2"
skalberg@14516
    37
  "TWOEXP_MONO" > "HOL4Word32.bits.TWOEXP_MONO"
skalberg@14516
    38
  "TWOEXP_DIVISION" > "HOL4Word32.bits.TWOEXP_DIVISION"
skalberg@14516
    39
  "TIMES_2EXP_primdef" > "HOL4Word32.bits.TIMES_2EXP_primdef"
skalberg@14516
    40
  "TIMES_2EXP_def" > "HOL4Word32.bits.TIMES_2EXP_def"
skalberg@14516
    41
  "SUC_SUB" > "HOL4Word32.bits.SUC_SUB"
skalberg@14516
    42
  "SLICE_primdef" > "HOL4Word32.bits.SLICE_primdef"
skalberg@14516
    43
  "SLICE_def" > "HOL4Word32.bits.SLICE_def"
skalberg@14516
    44
  "SLICE_ZERO" > "HOL4Word32.bits.SLICE_ZERO"
skalberg@14516
    45
  "SLICE_THM" > "HOL4Word32.bits.SLICE_THM"
skalberg@14516
    46
  "SLICE_LEM3" > "HOL4Word32.bits.SLICE_LEM3"
skalberg@14516
    47
  "SLICE_LEM2" > "HOL4Word32.bits.SLICE_LEM2"
skalberg@14516
    48
  "SLICE_LEM1" > "HOL4Word32.bits.SLICE_LEM1"
skalberg@14516
    49
  "SLICE_COMP_THM" > "HOL4Word32.bits.SLICE_COMP_THM"
skalberg@14516
    50
  "SLICELT_THM" > "HOL4Word32.bits.SLICELT_THM"
skalberg@14516
    51
  "SBIT_primdef" > "HOL4Word32.bits.SBIT_primdef"
skalberg@14516
    52
  "SBIT_def" > "HOL4Word32.bits.SBIT_def"
skalberg@14516
    53
  "SBIT_DIV" > "HOL4Word32.bits.SBIT_DIV"
skalberg@14516
    54
  "ODD_MOD2_LEM" > "HOL4Word32.bits.ODD_MOD2_LEM"
skalberg@14516
    55
  "NOT_ZERO_ADD1" > "Nat.not0_implies_Suc"
skalberg@14516
    56
  "NOT_MOD2_LEM2" > "HOL4Word32.bits.NOT_MOD2_LEM2"
skalberg@14516
    57
  "NOT_MOD2_LEM" > "HOL4Word32.bits.NOT_MOD2_LEM"
skalberg@14516
    58
  "NOT_BITS2" > "HOL4Word32.bits.NOT_BITS2"
skalberg@14516
    59
  "NOT_BITS" > "HOL4Word32.bits.NOT_BITS"
skalberg@14516
    60
  "NOT_BIT" > "HOL4Word32.bits.NOT_BIT"
skalberg@14516
    61
  "MOD_PLUS_RIGHT" > "HOL4Word32.bits.MOD_PLUS_RIGHT"
skalberg@14516
    62
  "MOD_PLUS_1" > "HOL4Word32.bits.MOD_PLUS_1"
skalberg@14516
    63
  "MOD_ADD_1" > "HOL4Word32.bits.MOD_ADD_1"
skalberg@14516
    64
  "MOD_2EXP_primdef" > "HOL4Word32.bits.MOD_2EXP_primdef"
skalberg@14516
    65
  "MOD_2EXP_def" > "HOL4Word32.bits.MOD_2EXP_def"
skalberg@14516
    66
  "MOD_2EXP_MONO" > "HOL4Word32.bits.MOD_2EXP_MONO"
skalberg@14516
    67
  "MOD_2EXP_LT" > "HOL4Word32.bits.MOD_2EXP_LT"
skalberg@14516
    68
  "MOD_2EXP_LEM" > "HOL4Word32.bits.MOD_2EXP_LEM"
skalberg@14516
    69
  "LSBn_primdef" > "HOL4Word32.bits.LSBn_primdef"
skalberg@14516
    70
  "LSBn_def" > "HOL4Word32.bits.LSBn_def"
skalberg@14516
    71
  "LSB_ODD" > "HOL4Word32.bits.LSB_ODD"
skalberg@14516
    72
  "LESS_EXP_MULT2" > "HOL4Word32.bits.LESS_EXP_MULT2"
skalberg@14516
    73
  "LESS_EQ_EXP_MULT" > "HOL4Word32.bits.LESS_EQ_EXP_MULT"
skalberg@14516
    74
  "EXP_SUB_LESS_EQ" > "HOL4Word32.bits.EXP_SUB_LESS_EQ"
skalberg@14516
    75
  "EVEN_MOD2_LEM" > "HOL4Word32.bits.EVEN_MOD2_LEM"
skalberg@14516
    76
  "DIV_MULT_THM2" > "HOL4Word32.bits.DIV_MULT_THM2"
skalberg@14516
    77
  "DIV_MULT_THM" > "HOL4Word32.bits.DIV_MULT_THM"
skalberg@14516
    78
  "DIV_MULT_LEM" > "HOL4Word32.bits.DIV_MULT_LEM"
skalberg@14516
    79
  "DIV_MULT_1" > "HOL4Word32.bits.DIV_MULT_1"
skalberg@14516
    80
  "DIV_2EXP_primdef" > "HOL4Word32.bits.DIV_2EXP_primdef"
skalberg@14516
    81
  "DIV_2EXP_def" > "HOL4Word32.bits.DIV_2EXP_def"
skalberg@14516
    82
  "DIVMOD_2EXP_primdef" > "HOL4Word32.bits.DIVMOD_2EXP_primdef"
skalberg@14516
    83
  "DIVMOD_2EXP_def" > "HOL4Word32.bits.DIVMOD_2EXP_def"
skalberg@14516
    84
  "DIV2_primdef" > "HOL4Word32.bits.DIV2_primdef"
skalberg@14516
    85
  "DIV2_def" > "HOL4Word32.bits.DIV2_def"
skalberg@14516
    86
  "DIV1" > "HOL4Word32.bits.DIV1"
skalberg@14516
    87
  "BIT_def" > "HOL4Word32.bits.BIT_def"
skalberg@14516
    88
  "BIT_SLICE_THM" > "HOL4Word32.bits.BIT_SLICE_THM"
skalberg@14516
    89
  "BIT_SLICE_LEM" > "HOL4Word32.bits.BIT_SLICE_LEM"
skalberg@14516
    90
  "BIT_SLICE" > "HOL4Word32.bits.BIT_SLICE"
skalberg@14516
    91
  "BIT_COMP_THM3" > "HOL4Word32.bits.BIT_COMP_THM3"
skalberg@14516
    92
  "BIT_BITS_THM" > "HOL4Word32.bits.BIT_BITS_THM"
skalberg@14516
    93
  "BITWISE_def" > "HOL4Word32.bits.BITWISE_def"
skalberg@14516
    94
  "BITWISE_THM" > "HOL4Word32.bits.BITWISE_THM"
skalberg@14516
    95
  "BITWISE_NOT_COR" > "HOL4Word32.bits.BITWISE_NOT_COR"
skalberg@14516
    96
  "BITWISE_LT_2EXP" > "HOL4Word32.bits.BITWISE_LT_2EXP"
skalberg@14516
    97
  "BITWISE_COR" > "HOL4Word32.bits.BITWISE_COR"
skalberg@14516
    98
  "BITS_primdef" > "HOL4Word32.bits.BITS_primdef"
skalberg@14516
    99
  "BITS_def" > "HOL4Word32.bits.BITS_def"
skalberg@14516
   100
  "BITS_ZERO3" > "HOL4Word32.bits.BITS_ZERO3"
skalberg@14516
   101
  "BITS_ZERO2" > "HOL4Word32.bits.BITS_ZERO2"
skalberg@14516
   102
  "BITS_ZERO" > "HOL4Word32.bits.BITS_ZERO"
skalberg@14516
   103
  "BITS_THM" > "HOL4Word32.bits.BITS_THM"
skalberg@14516
   104
  "BITS_SUC_THM" > "HOL4Word32.bits.BITS_SUC_THM"
skalberg@14516
   105
  "BITS_SUC" > "HOL4Word32.bits.BITS_SUC"
skalberg@14516
   106
  "BITS_SLICE_THM2" > "HOL4Word32.bits.BITS_SLICE_THM2"
skalberg@14516
   107
  "BITS_SLICE_THM" > "HOL4Word32.bits.BITS_SLICE_THM"
skalberg@14516
   108
  "BITS_LT_HIGH" > "HOL4Word32.bits.BITS_LT_HIGH"
skalberg@14516
   109
  "BITS_DIV_THM" > "HOL4Word32.bits.BITS_DIV_THM"
skalberg@14516
   110
  "BITS_COMP_THM2" > "HOL4Word32.bits.BITS_COMP_THM2"
skalberg@14516
   111
  "BITS_COMP_THM" > "HOL4Word32.bits.BITS_COMP_THM"
skalberg@14516
   112
  "BITSLT_THM" > "HOL4Word32.bits.BITSLT_THM"
skalberg@14516
   113
  "BITS2_THM" > "HOL4Word32.bits.BITS2_THM"
skalberg@14516
   114
skalberg@14516
   115
end