src/HOL/Import/HOL/word_base.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
skalberg@14516
     1
import
skalberg@14516
     2
skalberg@14516
     3
import_segment "hol4"
skalberg@14516
     4
skalberg@14516
     5
def_maps
skalberg@14516
     6
  "word_size" > "word_size_primdef"
skalberg@14516
     7
  "word_case" > "word_case_primdef"
skalberg@14516
     8
  "word_base0" > "word_base0_primdef"
skalberg@14516
     9
  "mk_word" > "mk_word_def"
skalberg@14516
    10
  "dest_word" > "dest_word_def"
skalberg@14516
    11
  "bit" > "bit_def"
skalberg@14516
    12
  "WSPLIT" > "WSPLIT_def"
skalberg@14516
    13
  "WSEG" > "WSEG_def"
skalberg@14516
    14
  "WORDLEN" > "WORDLEN_def"
skalberg@14516
    15
  "WORD" > "WORD_def"
skalberg@14516
    16
  "WCAT" > "WCAT_def"
skalberg@14516
    17
  "PWORDLEN" > "PWORDLEN_primdef"
skalberg@14516
    18
  "MSB" > "MSB_def"
skalberg@14516
    19
  "LSB" > "LSB_def"
skalberg@14516
    20
skalberg@14516
    21
type_maps
skalberg@14516
    22
  "word" > "HOL4Vec.word_base.word"
skalberg@14516
    23
skalberg@14516
    24
const_maps
skalberg@14516
    25
  "word_base0" > "HOL4Vec.word_base.word_base0"
skalberg@14516
    26
  "WORD" > "HOL4Vec.word_base.WORD"
skalberg@14516
    27
  "PWORDLEN" > "HOL4Vec.word_base.PWORDLEN"
skalberg@14516
    28
skalberg@14516
    29
const_renames
skalberg@14516
    30
  "BIT" > "bit"
skalberg@14516
    31
skalberg@14516
    32
thm_maps
skalberg@14516
    33
  "word_size_def" > "HOL4Vec.word_base.word_size_def"
skalberg@14516
    34
  "word_repfns" > "HOL4Vec.word_base.word_repfns"
skalberg@14516
    35
  "word_nchotomy" > "HOL4Vec.word_base.word_nchotomy"
skalberg@14516
    36
  "word_induction" > "HOL4Vec.word_base.word_induction"
skalberg@14516
    37
  "word_induct" > "HOL4Vec.word_base.word_induct"
skalberg@14516
    38
  "word_cases" > "HOL4Vec.word_base.word_cases"
skalberg@14516
    39
  "word_case_def" > "HOL4Vec.word_base.word_case_def"
skalberg@14516
    40
  "word_case_cong" > "HOL4Vec.word_base.word_case_cong"
skalberg@14516
    41
  "word_base0_primdef" > "HOL4Vec.word_base.word_base0_primdef"
skalberg@14516
    42
  "word_base0_def" > "HOL4Vec.word_base.word_base0_def"
skalberg@14516
    43
  "word_TY_DEF" > "HOL4Vec.word_base.word_TY_DEF"
skalberg@14516
    44
  "word_Axiom" > "HOL4Vec.word_base.word_Axiom"
skalberg@14516
    45
  "word_Ax" > "HOL4Vec.word_base.word_Ax"
skalberg@14516
    46
  "word_11" > "HOL4Vec.word_base.word_11"
skalberg@14516
    47
  "WSPLIT_WSEG2" > "HOL4Vec.word_base.WSPLIT_WSEG2"
skalberg@14516
    48
  "WSPLIT_WSEG1" > "HOL4Vec.word_base.WSPLIT_WSEG1"
skalberg@14516
    49
  "WSPLIT_WSEG" > "HOL4Vec.word_base.WSPLIT_WSEG"
skalberg@14516
    50
  "WSPLIT_PWORDLEN" > "HOL4Vec.word_base.WSPLIT_PWORDLEN"
skalberg@14516
    51
  "WSPLIT_DEF" > "HOL4Vec.word_base.WSPLIT_DEF"
skalberg@14516
    52
  "WSEG_WSEG" > "HOL4Vec.word_base.WSEG_WSEG"
skalberg@14516
    53
  "WSEG_WORD_LENGTH" > "HOL4Vec.word_base.WSEG_WORD_LENGTH"
skalberg@14516
    54
  "WSEG_WORDLEN" > "HOL4Vec.word_base.WSEG_WORDLEN"
skalberg@14516
    55
  "WSEG_WCAT_WSEG2" > "HOL4Vec.word_base.WSEG_WCAT_WSEG2"
skalberg@14516
    56
  "WSEG_WCAT_WSEG1" > "HOL4Vec.word_base.WSEG_WCAT_WSEG1"
skalberg@14516
    57
  "WSEG_WCAT_WSEG" > "HOL4Vec.word_base.WSEG_WCAT_WSEG"
skalberg@14516
    58
  "WSEG_WCAT2" > "HOL4Vec.word_base.WSEG_WCAT2"
skalberg@14516
    59
  "WSEG_WCAT1" > "HOL4Vec.word_base.WSEG_WCAT1"
skalberg@14516
    60
  "WSEG_SUC" > "HOL4Vec.word_base.WSEG_SUC"
skalberg@14516
    61
  "WSEG_PWORDLEN" > "HOL4Vec.word_base.WSEG_PWORDLEN"
skalberg@14516
    62
  "WSEG_DEF" > "HOL4Vec.word_base.WSEG_DEF"
skalberg@14516
    63
  "WSEG_BIT" > "HOL4Vec.word_base.WSEG_BIT"
skalberg@14516
    64
  "WSEG0" > "HOL4Vec.word_base.WSEG0"
skalberg@14516
    65
  "WORD_def" > "HOL4Vec.word_base.WORD_def"
skalberg@14516
    66
  "WORD_SPLIT" > "HOL4Vec.word_base.WORD_SPLIT"
skalberg@14516
    67
  "WORD_SNOC_WCAT" > "HOL4Vec.word_base.WORD_SNOC_WCAT"
skalberg@14516
    68
  "WORD_PARTITION" > "HOL4Vec.word_base.WORD_PARTITION"
skalberg@14516
    69
  "WORD_CONS_WCAT" > "HOL4Vec.word_base.WORD_CONS_WCAT"
skalberg@14516
    70
  "WORD_11" > "HOL4Vec.word_base.WORD_11"
skalberg@14516
    71
  "WORDLEN_SUC_WCAT_WSEG_WSEG_RIGHT" > "HOL4Vec.word_base.WORDLEN_SUC_WCAT_WSEG_WSEG_RIGHT"
skalberg@14516
    72
  "WORDLEN_SUC_WCAT_WSEG_WSEG" > "HOL4Vec.word_base.WORDLEN_SUC_WCAT_WSEG_WSEG"
skalberg@14516
    73
  "WORDLEN_SUC_WCAT_BIT_WSEG_RIGHT" > "HOL4Vec.word_base.WORDLEN_SUC_WCAT_BIT_WSEG_RIGHT"
skalberg@14516
    74
  "WORDLEN_SUC_WCAT_BIT_WSEG" > "HOL4Vec.word_base.WORDLEN_SUC_WCAT_BIT_WSEG"
skalberg@14516
    75
  "WORDLEN_SUC_WCAT" > "HOL4Vec.word_base.WORDLEN_SUC_WCAT"
skalberg@14516
    76
  "WORDLEN_DEF" > "HOL4Vec.word_base.WORDLEN_DEF"
skalberg@14516
    77
  "WORD" > "HOL4Vec.word_base.WORD"
skalberg@14516
    78
  "WCAT_WSEG_WSEG" > "HOL4Vec.word_base.WCAT_WSEG_WSEG"
skalberg@14516
    79
  "WCAT_PWORDLEN" > "HOL4Vec.word_base.WCAT_PWORDLEN"
skalberg@14516
    80
  "WCAT_DEF" > "HOL4Vec.word_base.WCAT_DEF"
skalberg@14516
    81
  "WCAT_ASSOC" > "HOL4Vec.word_base.WCAT_ASSOC"
skalberg@14516
    82
  "WCAT_11" > "HOL4Vec.word_base.WCAT_11"
skalberg@14516
    83
  "WCAT0" > "HOL4Vec.word_base.WCAT0"
skalberg@14516
    84
  "PWORDLEN_primdef" > "HOL4Vec.word_base.PWORDLEN_primdef"
skalberg@14516
    85
  "PWORDLEN_def" > "HOL4Vec.word_base.PWORDLEN_def"
skalberg@14516
    86
  "PWORDLEN1" > "HOL4Vec.word_base.PWORDLEN1"
skalberg@14516
    87
  "PWORDLEN0" > "HOL4Vec.word_base.PWORDLEN0"
skalberg@14516
    88
  "PWORDLEN" > "HOL4Vec.word_base.PWORDLEN"
skalberg@14516
    89
  "MSB_DEF" > "HOL4Vec.word_base.MSB_DEF"
skalberg@14516
    90
  "MSB" > "HOL4Vec.word_base.MSB"
skalberg@14516
    91
  "LSB_DEF" > "HOL4Vec.word_base.LSB_DEF"
skalberg@14516
    92
  "LSB" > "HOL4Vec.word_base.LSB"
skalberg@14516
    93
  "IN_PWORDLEN" > "HOL4Vec.word_base.IN_PWORDLEN"
skalberg@14516
    94
  "BIT_WSEG" > "HOL4Vec.word_base.BIT_WSEG"
skalberg@14516
    95
  "BIT_WCAT_SND" > "HOL4Vec.word_base.BIT_WCAT_SND"
skalberg@14516
    96
  "BIT_WCAT_FST" > "HOL4Vec.word_base.BIT_WCAT_FST"
skalberg@14516
    97
  "BIT_WCAT1" > "HOL4Vec.word_base.BIT_WCAT1"
skalberg@14516
    98
  "BIT_EQ_IMP_WORD_EQ" > "HOL4Vec.word_base.BIT_EQ_IMP_WORD_EQ"
skalberg@14516
    99
  "BIT_DEF" > "HOL4Vec.word_base.BIT_DEF"
skalberg@14516
   100
  "BIT0" > "HOL4Vec.word_base.BIT0"
skalberg@14516
   101
skalberg@14516
   102
end