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