src/HOL/Import/HOL/hreal.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
  "isacut" > "isacut_def"
skalberg@14516
     7
  "hreal_sup" > "hreal_sup_def"
skalberg@14516
     8
  "hreal_sub" > "hreal_sub_def"
skalberg@14516
     9
  "hreal_mul" > "hreal_mul_def"
skalberg@14516
    10
  "hreal_lt" > "hreal_lt_def"
skalberg@14516
    11
  "hreal_inv" > "hreal_inv_def"
skalberg@14516
    12
  "hreal_add" > "hreal_add_def"
skalberg@14516
    13
  "hreal_1" > "hreal_1_def"
skalberg@14516
    14
  "hreal" > "hreal_def"
skalberg@14516
    15
  "hrat_lt" > "hrat_lt_def"
skalberg@14516
    16
  "cut_of_hrat" > "cut_of_hrat_def"
skalberg@14516
    17
  "cut" > "cut_def"
skalberg@14516
    18
skalberg@14516
    19
type_maps
skalberg@14516
    20
  "hreal" > "HOL4Base.hreal.hreal"
skalberg@14516
    21
skalberg@14516
    22
const_maps
skalberg@14516
    23
  "isacut" > "HOL4Base.hreal.isacut"
skalberg@14516
    24
  "hreal_sup" > "HOL4Base.hreal.hreal_sup"
skalberg@14516
    25
  "hreal_sub" > "HOL4Base.hreal.hreal_sub"
skalberg@14516
    26
  "hreal_mul" > "HOL4Base.hreal.hreal_mul"
skalberg@14516
    27
  "hreal_lt" > "HOL4Base.hreal.hreal_lt"
skalberg@14516
    28
  "hreal_inv" > "HOL4Base.hreal.hreal_inv"
skalberg@14516
    29
  "hreal_add" > "HOL4Base.hreal.hreal_add"
skalberg@14516
    30
  "hreal_1" > "HOL4Base.hreal.hreal_1"
skalberg@14516
    31
  "hrat_lt" > "HOL4Base.hreal.hrat_lt"
skalberg@14516
    32
  "cut_of_hrat" > "HOL4Base.hreal.cut_of_hrat"
skalberg@14516
    33
skalberg@14516
    34
thm_maps
skalberg@14516
    35
  "isacut_def" > "HOL4Base.hreal.isacut_def"
skalberg@14516
    36
  "isacut" > "HOL4Base.hreal.isacut"
skalberg@14516
    37
  "hreal_tybij" > "HOL4Base.hreal.hreal_tybij"
skalberg@14516
    38
  "hreal_sup_def" > "HOL4Base.hreal.hreal_sup_def"
skalberg@14516
    39
  "hreal_sup" > "HOL4Base.hreal.hreal_sup"
skalberg@14516
    40
  "hreal_sub_def" > "HOL4Base.hreal.hreal_sub_def"
skalberg@14516
    41
  "hreal_sub" > "HOL4Base.hreal.hreal_sub"
skalberg@14516
    42
  "hreal_mul_def" > "HOL4Base.hreal.hreal_mul_def"
skalberg@14516
    43
  "hreal_mul" > "HOL4Base.hreal.hreal_mul"
skalberg@14516
    44
  "hreal_lt_def" > "HOL4Base.hreal.hreal_lt_def"
skalberg@14516
    45
  "hreal_lt" > "HOL4Base.hreal.hreal_lt"
skalberg@14516
    46
  "hreal_inv_def" > "HOL4Base.hreal.hreal_inv_def"
skalberg@14516
    47
  "hreal_inv" > "HOL4Base.hreal.hreal_inv"
skalberg@14516
    48
  "hreal_add_def" > "HOL4Base.hreal.hreal_add_def"
skalberg@14516
    49
  "hreal_add" > "HOL4Base.hreal.hreal_add"
skalberg@14516
    50
  "hreal_TY_DEF" > "HOL4Base.hreal.hreal_TY_DEF"
skalberg@14516
    51
  "hreal_1_def" > "HOL4Base.hreal.hreal_1_def"
skalberg@14516
    52
  "hreal_1" > "HOL4Base.hreal.hreal_1"
skalberg@14516
    53
  "hrat_lt_def" > "HOL4Base.hreal.hrat_lt_def"
skalberg@14516
    54
  "hrat_lt" > "HOL4Base.hreal.hrat_lt"
skalberg@14516
    55
  "cut_of_hrat_def" > "HOL4Base.hreal.cut_of_hrat_def"
skalberg@14516
    56
  "cut_of_hrat" > "HOL4Base.hreal.cut_of_hrat"
skalberg@14516
    57
  "ISACUT_HRAT" > "HOL4Base.hreal.ISACUT_HRAT"
skalberg@14516
    58
  "HREAL_SUP_ISACUT" > "HOL4Base.hreal.HREAL_SUP_ISACUT"
skalberg@14516
    59
  "HREAL_SUP" > "HOL4Base.hreal.HREAL_SUP"
skalberg@14516
    60
  "HREAL_SUB_ISACUT" > "HOL4Base.hreal.HREAL_SUB_ISACUT"
skalberg@14516
    61
  "HREAL_SUB_ADD" > "HOL4Base.hreal.HREAL_SUB_ADD"
skalberg@14516
    62
  "HREAL_NOZERO" > "HOL4Base.hreal.HREAL_NOZERO"
skalberg@14516
    63
  "HREAL_MUL_SYM" > "HOL4Base.hreal.HREAL_MUL_SYM"
skalberg@14516
    64
  "HREAL_MUL_LINV" > "HOL4Base.hreal.HREAL_MUL_LINV"
skalberg@14516
    65
  "HREAL_MUL_LID" > "HOL4Base.hreal.HREAL_MUL_LID"
skalberg@14516
    66
  "HREAL_MUL_ISACUT" > "HOL4Base.hreal.HREAL_MUL_ISACUT"
skalberg@14516
    67
  "HREAL_MUL_ASSOC" > "HOL4Base.hreal.HREAL_MUL_ASSOC"
skalberg@14516
    68
  "HREAL_LT_TOTAL" > "HOL4Base.hreal.HREAL_LT_TOTAL"
skalberg@14516
    69
  "HREAL_LT_LEMMA" > "HOL4Base.hreal.HREAL_LT_LEMMA"
skalberg@14516
    70
  "HREAL_LT" > "HOL4Base.hreal.HREAL_LT"
skalberg@14516
    71
  "HREAL_LDISTRIB" > "HOL4Base.hreal.HREAL_LDISTRIB"
skalberg@14516
    72
  "HREAL_INV_ISACUT" > "HOL4Base.hreal.HREAL_INV_ISACUT"
skalberg@14516
    73
  "HREAL_ADD_TOTAL" > "HOL4Base.hreal.HREAL_ADD_TOTAL"
skalberg@14516
    74
  "HREAL_ADD_SYM" > "HOL4Base.hreal.HREAL_ADD_SYM"
skalberg@14516
    75
  "HREAL_ADD_ISACUT" > "HOL4Base.hreal.HREAL_ADD_ISACUT"
skalberg@14516
    76
  "HREAL_ADD_ASSOC" > "HOL4Base.hreal.HREAL_ADD_ASSOC"
skalberg@14516
    77
  "HRAT_UP" > "HOL4Base.hreal.HRAT_UP"
skalberg@14516
    78
  "HRAT_RDISTRIB" > "HOL4Base.hreal.HRAT_RDISTRIB"
skalberg@14516
    79
  "HRAT_MUL_RINV" > "HOL4Base.hreal.HRAT_MUL_RINV"
skalberg@14516
    80
  "HRAT_MUL_RID" > "HOL4Base.hreal.HRAT_MUL_RID"
skalberg@14516
    81
  "HRAT_MEAN" > "HOL4Base.hreal.HRAT_MEAN"
skalberg@14516
    82
  "HRAT_LT_TRANS" > "HOL4Base.hreal.HRAT_LT_TRANS"
skalberg@14516
    83
  "HRAT_LT_TOTAL" > "HOL4Base.hreal.HRAT_LT_TOTAL"
skalberg@14516
    84
  "HRAT_LT_RMUL1" > "HOL4Base.hreal.HRAT_LT_RMUL1"
skalberg@14516
    85
  "HRAT_LT_RMUL" > "HOL4Base.hreal.HRAT_LT_RMUL"
skalberg@14516
    86
  "HRAT_LT_REFL" > "HOL4Base.hreal.HRAT_LT_REFL"
skalberg@14516
    87
  "HRAT_LT_RADD" > "HOL4Base.hreal.HRAT_LT_RADD"
skalberg@14516
    88
  "HRAT_LT_R1" > "HOL4Base.hreal.HRAT_LT_R1"
skalberg@14516
    89
  "HRAT_LT_NE" > "HOL4Base.hreal.HRAT_LT_NE"
skalberg@14516
    90
  "HRAT_LT_MUL2" > "HOL4Base.hreal.HRAT_LT_MUL2"
skalberg@14516
    91
  "HRAT_LT_LMUL1" > "HOL4Base.hreal.HRAT_LT_LMUL1"
skalberg@14516
    92
  "HRAT_LT_LMUL" > "HOL4Base.hreal.HRAT_LT_LMUL"
skalberg@14516
    93
  "HRAT_LT_LADD" > "HOL4Base.hreal.HRAT_LT_LADD"
skalberg@14516
    94
  "HRAT_LT_L1" > "HOL4Base.hreal.HRAT_LT_L1"
skalberg@14516
    95
  "HRAT_LT_GT" > "HOL4Base.hreal.HRAT_LT_GT"
skalberg@14516
    96
  "HRAT_LT_ANTISYM" > "HOL4Base.hreal.HRAT_LT_ANTISYM"
skalberg@14516
    97
  "HRAT_LT_ADDR" > "HOL4Base.hreal.HRAT_LT_ADDR"
skalberg@14516
    98
  "HRAT_LT_ADDL" > "HOL4Base.hreal.HRAT_LT_ADDL"
skalberg@14516
    99
  "HRAT_LT_ADD2" > "HOL4Base.hreal.HRAT_LT_ADD2"
skalberg@14516
   100
  "HRAT_INV_MUL" > "HOL4Base.hreal.HRAT_INV_MUL"
skalberg@14516
   101
  "HRAT_GT_LMUL1" > "HOL4Base.hreal.HRAT_GT_LMUL1"
skalberg@14516
   102
  "HRAT_GT_L1" > "HOL4Base.hreal.HRAT_GT_L1"
skalberg@14516
   103
  "HRAT_EQ_LMUL" > "HOL4Base.hreal.HRAT_EQ_LMUL"
skalberg@14516
   104
  "HRAT_EQ_LADD" > "HOL4Base.hreal.HRAT_EQ_LADD"
skalberg@14516
   105
  "HRAT_DOWN2" > "HOL4Base.hreal.HRAT_DOWN2"
skalberg@14516
   106
  "HRAT_DOWN" > "HOL4Base.hreal.HRAT_DOWN"
skalberg@14516
   107
  "EQUAL_CUTS" > "HOL4Base.hreal.EQUAL_CUTS"
skalberg@14516
   108
  "CUT_UP" > "HOL4Base.hreal.CUT_UP"
skalberg@14516
   109
  "CUT_UBOUND" > "HOL4Base.hreal.CUT_UBOUND"
skalberg@14516
   110
  "CUT_STRADDLE" > "HOL4Base.hreal.CUT_STRADDLE"
skalberg@14516
   111
  "CUT_NONEMPTY" > "HOL4Base.hreal.CUT_NONEMPTY"
skalberg@14516
   112
  "CUT_NEARTOP_MUL" > "HOL4Base.hreal.CUT_NEARTOP_MUL"
skalberg@14516
   113
  "CUT_NEARTOP_ADD" > "HOL4Base.hreal.CUT_NEARTOP_ADD"
skalberg@14516
   114
  "CUT_ISACUT" > "HOL4Base.hreal.CUT_ISACUT"
skalberg@14516
   115
  "CUT_DOWN" > "HOL4Base.hreal.CUT_DOWN"
skalberg@14516
   116
  "CUT_BOUNDED" > "HOL4Base.hreal.CUT_BOUNDED"
skalberg@14516
   117
skalberg@14516
   118
end