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