src/HOL/Import/HOL/lim.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 14516 a183dec876ab
child 44763 b50d5d694838
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
  "tends_real_real" > "tends_real_real_def"
skalberg@14516
     7
  "diffl" > "diffl_def"
skalberg@14516
     8
  "differentiable" > "differentiable_def"
skalberg@14516
     9
  "contl" > "contl_def"
skalberg@14516
    10
skalberg@14516
    11
const_maps
skalberg@14516
    12
  "tends_real_real" > "HOL4Real.lim.tends_real_real"
skalberg@14516
    13
  "diffl" > "HOL4Real.lim.diffl"
skalberg@14516
    14
  "differentiable" > "HOL4Real.lim.differentiable"
skalberg@14516
    15
  "contl" > "HOL4Real.lim.contl"
skalberg@14516
    16
skalberg@14516
    17
thm_maps
skalberg@14516
    18
  "tends_real_real_def" > "HOL4Real.lim.tends_real_real_def"
skalberg@14516
    19
  "tends_real_real" > "HOL4Real.lim.tends_real_real"
skalberg@14516
    20
  "diffl_def" > "HOL4Real.lim.diffl_def"
skalberg@14516
    21
  "diffl" > "HOL4Real.lim.diffl"
skalberg@14516
    22
  "differentiable_def" > "HOL4Real.lim.differentiable_def"
skalberg@14516
    23
  "differentiable" > "HOL4Real.lim.differentiable"
skalberg@14516
    24
  "contl_def" > "HOL4Real.lim.contl_def"
skalberg@14516
    25
  "contl" > "HOL4Real.lim.contl"
skalberg@14516
    26
  "ROLLE" > "HOL4Real.lim.ROLLE"
skalberg@14516
    27
  "MVT_LEMMA" > "HOL4Real.lim.MVT_LEMMA"
skalberg@14516
    28
  "MVT" > "HOL4Real.lim.MVT"
skalberg@14516
    29
  "LIM_X" > "HOL4Real.lim.LIM_X"
skalberg@14516
    30
  "LIM_UNIQ" > "HOL4Real.lim.LIM_UNIQ"
skalberg@14516
    31
  "LIM_TRANSFORM" > "HOL4Real.lim.LIM_TRANSFORM"
skalberg@14516
    32
  "LIM_SUB" > "HOL4Real.lim.LIM_SUB"
skalberg@14516
    33
  "LIM_NULL" > "HOL4Real.lim.LIM_NULL"
skalberg@14516
    34
  "LIM_NEG" > "HOL4Real.lim.LIM_NEG"
skalberg@14516
    35
  "LIM_MUL" > "HOL4Real.lim.LIM_MUL"
skalberg@14516
    36
  "LIM_INV" > "HOL4Real.lim.LIM_INV"
skalberg@14516
    37
  "LIM_EQUAL" > "HOL4Real.lim.LIM_EQUAL"
skalberg@14516
    38
  "LIM_DIV" > "HOL4Real.lim.LIM_DIV"
skalberg@14516
    39
  "LIM_CONST" > "HOL4Real.lim.LIM_CONST"
skalberg@14516
    40
  "LIM_ADD" > "HOL4Real.lim.LIM_ADD"
skalberg@14516
    41
  "LIM" > "HOL4Real.lim.LIM"
skalberg@14516
    42
  "IVT2" > "HOL4Real.lim.IVT2"
skalberg@14516
    43
  "IVT" > "HOL4Real.lim.IVT"
skalberg@14516
    44
  "INTERVAL_LEMMA" > "HOL4Real.lim.INTERVAL_LEMMA"
skalberg@14516
    45
  "INTERVAL_CLEMMA" > "HOL4Real.lim.INTERVAL_CLEMMA"
skalberg@14516
    46
  "INTERVAL_ABS" > "HOL4Real.lim.INTERVAL_ABS"
skalberg@14516
    47
  "DIFF_XM1" > "HOL4Real.lim.DIFF_XM1"
skalberg@14516
    48
  "DIFF_X" > "HOL4Real.lim.DIFF_X"
skalberg@14516
    49
  "DIFF_UNIQ" > "HOL4Real.lim.DIFF_UNIQ"
skalberg@14516
    50
  "DIFF_SUM" > "HOL4Real.lim.DIFF_SUM"
skalberg@14516
    51
  "DIFF_SUB" > "HOL4Real.lim.DIFF_SUB"
skalberg@14516
    52
  "DIFF_POW" > "HOL4Real.lim.DIFF_POW"
skalberg@14516
    53
  "DIFF_NEG" > "HOL4Real.lim.DIFF_NEG"
skalberg@14516
    54
  "DIFF_MUL" > "HOL4Real.lim.DIFF_MUL"
skalberg@14516
    55
  "DIFF_LMIN" > "HOL4Real.lim.DIFF_LMIN"
skalberg@14516
    56
  "DIFF_LMAX" > "HOL4Real.lim.DIFF_LMAX"
skalberg@14516
    57
  "DIFF_LINC" > "HOL4Real.lim.DIFF_LINC"
skalberg@14516
    58
  "DIFF_LDEC" > "HOL4Real.lim.DIFF_LDEC"
skalberg@14516
    59
  "DIFF_LCONST" > "HOL4Real.lim.DIFF_LCONST"
skalberg@14516
    60
  "DIFF_ISCONST_END" > "HOL4Real.lim.DIFF_ISCONST_END"
skalberg@14516
    61
  "DIFF_ISCONST_ALL" > "HOL4Real.lim.DIFF_ISCONST_ALL"
skalberg@14516
    62
  "DIFF_ISCONST" > "HOL4Real.lim.DIFF_ISCONST"
skalberg@14516
    63
  "DIFF_INVERSE_OPEN" > "HOL4Real.lim.DIFF_INVERSE_OPEN"
skalberg@14516
    64
  "DIFF_INVERSE_LT" > "HOL4Real.lim.DIFF_INVERSE_LT"
skalberg@14516
    65
  "DIFF_INVERSE" > "HOL4Real.lim.DIFF_INVERSE"
skalberg@14516
    66
  "DIFF_INV" > "HOL4Real.lim.DIFF_INV"
skalberg@14516
    67
  "DIFF_DIV" > "HOL4Real.lim.DIFF_DIV"
skalberg@14516
    68
  "DIFF_CONT" > "HOL4Real.lim.DIFF_CONT"
skalberg@14516
    69
  "DIFF_CONST" > "HOL4Real.lim.DIFF_CONST"
skalberg@14516
    70
  "DIFF_CMUL" > "HOL4Real.lim.DIFF_CMUL"
skalberg@14516
    71
  "DIFF_CHAIN" > "HOL4Real.lim.DIFF_CHAIN"
skalberg@14516
    72
  "DIFF_CARAT" > "HOL4Real.lim.DIFF_CARAT"
skalberg@14516
    73
  "DIFF_ADD" > "HOL4Real.lim.DIFF_ADD"
skalberg@14516
    74
  "CONT_SUB" > "HOL4Real.lim.CONT_SUB"
skalberg@14516
    75
  "CONT_NEG" > "HOL4Real.lim.CONT_NEG"
skalberg@14516
    76
  "CONT_MUL" > "HOL4Real.lim.CONT_MUL"
skalberg@14516
    77
  "CONT_INVERSE" > "HOL4Real.lim.CONT_INVERSE"
skalberg@14516
    78
  "CONT_INV" > "HOL4Real.lim.CONT_INV"
skalberg@14516
    79
  "CONT_INJ_RANGE" > "HOL4Real.lim.CONT_INJ_RANGE"
skalberg@14516
    80
  "CONT_INJ_LEMMA2" > "HOL4Real.lim.CONT_INJ_LEMMA2"
skalberg@14516
    81
  "CONT_INJ_LEMMA" > "HOL4Real.lim.CONT_INJ_LEMMA"
skalberg@14516
    82
  "CONT_HASSUP" > "HOL4Real.lim.CONT_HASSUP"
skalberg@14516
    83
  "CONT_DIV" > "HOL4Real.lim.CONT_DIV"
skalberg@14516
    84
  "CONT_CONST" > "HOL4Real.lim.CONT_CONST"
skalberg@14516
    85
  "CONT_COMPOSE" > "HOL4Real.lim.CONT_COMPOSE"
skalberg@14516
    86
  "CONT_BOUNDED" > "HOL4Real.lim.CONT_BOUNDED"
skalberg@14516
    87
  "CONT_ATTAINS_ALL" > "HOL4Real.lim.CONT_ATTAINS_ALL"
skalberg@14516
    88
  "CONT_ATTAINS2" > "HOL4Real.lim.CONT_ATTAINS2"
skalberg@14516
    89
  "CONT_ATTAINS" > "HOL4Real.lim.CONT_ATTAINS"
skalberg@14516
    90
  "CONT_ADD" > "HOL4Real.lim.CONT_ADD"
skalberg@14516
    91
  "CONTL_LIM" > "HOL4Real.lim.CONTL_LIM"
skalberg@14516
    92
skalberg@14516
    93
end