src/HOL/Import/HOL/hrat.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   "trat_sucint" > "trat_sucint_def"
     7   "trat_mul" > "trat_mul_def"
     8   "trat_inv" > "trat_inv_def"
     9   "trat_eq" > "trat_eq_def"
    10   "trat_add" > "trat_add_def"
    11   "trat_1" > "trat_1_def"
    12   "mk_hrat" > "mk_hrat_def"
    13   "hrat_sucint" > "hrat_sucint_def"
    14   "hrat_mul" > "hrat_mul_def"
    15   "hrat_inv" > "hrat_inv_def"
    16   "hrat_add" > "hrat_add_def"
    17   "hrat_1" > "hrat_1_def"
    18   "dest_hrat" > "dest_hrat_def"
    19 
    20 type_maps
    21   "hrat" > "HOL4Base.hrat.hrat"
    22 
    23 const_maps
    24   "trat_mul" > "HOL4Base.hrat.trat_mul"
    25   "trat_inv" > "HOL4Base.hrat.trat_inv"
    26   "trat_eq" > "HOL4Base.hrat.trat_eq"
    27   "trat_add" > "HOL4Base.hrat.trat_add"
    28   "trat_1" > "HOL4Base.hrat.trat_1"
    29   "hrat_sucint" > "HOL4Base.hrat.hrat_sucint"
    30   "hrat_mul" > "HOL4Base.hrat.hrat_mul"
    31   "hrat_inv" > "HOL4Base.hrat.hrat_inv"
    32   "hrat_add" > "HOL4Base.hrat.hrat_add"
    33   "hrat_1" > "HOL4Base.hrat.hrat_1"
    34 
    35 thm_maps
    36   "trat_sucint" > "HOL4Base.hrat.trat_sucint"
    37   "trat_mul_def" > "HOL4Base.hrat.trat_mul_def"
    38   "trat_mul" > "HOL4Base.hrat.trat_mul"
    39   "trat_inv_def" > "HOL4Base.hrat.trat_inv_def"
    40   "trat_inv" > "HOL4Base.hrat.trat_inv"
    41   "trat_eq_def" > "HOL4Base.hrat.trat_eq_def"
    42   "trat_eq" > "HOL4Base.hrat.trat_eq"
    43   "trat_add_def" > "HOL4Base.hrat.trat_add_def"
    44   "trat_add" > "HOL4Base.hrat.trat_add"
    45   "trat_1_def" > "HOL4Base.hrat.trat_1_def"
    46   "trat_1" > "HOL4Base.hrat.trat_1"
    47   "hrat_tybij" > "HOL4Base.hrat.hrat_tybij"
    48   "hrat_sucint_def" > "HOL4Base.hrat.hrat_sucint_def"
    49   "hrat_sucint" > "HOL4Base.hrat.hrat_sucint"
    50   "hrat_mul_def" > "HOL4Base.hrat.hrat_mul_def"
    51   "hrat_mul" > "HOL4Base.hrat.hrat_mul"
    52   "hrat_inv_def" > "HOL4Base.hrat.hrat_inv_def"
    53   "hrat_inv" > "HOL4Base.hrat.hrat_inv"
    54   "hrat_add_def" > "HOL4Base.hrat.hrat_add_def"
    55   "hrat_add" > "HOL4Base.hrat.hrat_add"
    56   "hrat_TY_DEF" > "HOL4Base.hrat.hrat_TY_DEF"
    57   "hrat_1_def" > "HOL4Base.hrat.hrat_1_def"
    58   "hrat_1" > "HOL4Base.hrat.hrat_1"
    59   "TRAT_SUCINT_0" > "HOL4Base.hrat.TRAT_SUCINT_0"
    60   "TRAT_SUCINT" > "HOL4Base.hrat.TRAT_SUCINT"
    61   "TRAT_NOZERO" > "HOL4Base.hrat.TRAT_NOZERO"
    62   "TRAT_MUL_WELLDEFINED2" > "HOL4Base.hrat.TRAT_MUL_WELLDEFINED2"
    63   "TRAT_MUL_WELLDEFINED" > "HOL4Base.hrat.TRAT_MUL_WELLDEFINED"
    64   "TRAT_MUL_SYM_EQ" > "HOL4Base.hrat.TRAT_MUL_SYM_EQ"
    65   "TRAT_MUL_SYM" > "HOL4Base.hrat.TRAT_MUL_SYM"
    66   "TRAT_MUL_LINV" > "HOL4Base.hrat.TRAT_MUL_LINV"
    67   "TRAT_MUL_LID" > "HOL4Base.hrat.TRAT_MUL_LID"
    68   "TRAT_MUL_ASSOC" > "HOL4Base.hrat.TRAT_MUL_ASSOC"
    69   "TRAT_LDISTRIB" > "HOL4Base.hrat.TRAT_LDISTRIB"
    70   "TRAT_INV_WELLDEFINED" > "HOL4Base.hrat.TRAT_INV_WELLDEFINED"
    71   "TRAT_EQ_TRANS" > "HOL4Base.hrat.TRAT_EQ_TRANS"
    72   "TRAT_EQ_SYM" > "HOL4Base.hrat.TRAT_EQ_SYM"
    73   "TRAT_EQ_REFL" > "HOL4Base.hrat.TRAT_EQ_REFL"
    74   "TRAT_EQ_EQUIV" > "HOL4Base.hrat.TRAT_EQ_EQUIV"
    75   "TRAT_EQ_AP" > "HOL4Base.hrat.TRAT_EQ_AP"
    76   "TRAT_ARCH" > "HOL4Base.hrat.TRAT_ARCH"
    77   "TRAT_ADD_WELLDEFINED2" > "HOL4Base.hrat.TRAT_ADD_WELLDEFINED2"
    78   "TRAT_ADD_WELLDEFINED" > "HOL4Base.hrat.TRAT_ADD_WELLDEFINED"
    79   "TRAT_ADD_TOTAL" > "HOL4Base.hrat.TRAT_ADD_TOTAL"
    80   "TRAT_ADD_SYM_EQ" > "HOL4Base.hrat.TRAT_ADD_SYM_EQ"
    81   "TRAT_ADD_SYM" > "HOL4Base.hrat.TRAT_ADD_SYM"
    82   "TRAT_ADD_ASSOC" > "HOL4Base.hrat.TRAT_ADD_ASSOC"
    83   "HRAT_SUCINT" > "HOL4Base.hrat.HRAT_SUCINT"
    84   "HRAT_NOZERO" > "HOL4Base.hrat.HRAT_NOZERO"
    85   "HRAT_MUL_SYM" > "HOL4Base.hrat.HRAT_MUL_SYM"
    86   "HRAT_MUL_LINV" > "HOL4Base.hrat.HRAT_MUL_LINV"
    87   "HRAT_MUL_LID" > "HOL4Base.hrat.HRAT_MUL_LID"
    88   "HRAT_MUL_ASSOC" > "HOL4Base.hrat.HRAT_MUL_ASSOC"
    89   "HRAT_LDISTRIB" > "HOL4Base.hrat.HRAT_LDISTRIB"
    90   "HRAT_ARCH" > "HOL4Base.hrat.HRAT_ARCH"
    91   "HRAT_ADD_TOTAL" > "HOL4Base.hrat.HRAT_ADD_TOTAL"
    92   "HRAT_ADD_SYM" > "HOL4Base.hrat.HRAT_ADD_SYM"
    93   "HRAT_ADD_ASSOC" > "HOL4Base.hrat.HRAT_ADD_ASSOC"
    94 
    95 end