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