src/HOL/Import/HOL/seq.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 17694 b7870c2bd7df
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
  "sums" > "sums_def"
skalberg@14516
     7
  "summable" > "summable_def"
skalberg@14516
     8
  "suminf" > "suminf_def"
skalberg@14516
     9
  "subseq" > "subseq_def"
skalberg@14516
    10
  "mono" > "mono_def"
skalberg@14516
    11
  "lim" > "lim_def"
obua@17694
    12
  "hol4-->" > "hol4-->_def"
skalberg@14516
    13
  "convergent" > "convergent_def"
skalberg@14516
    14
  "cauchy" > "cauchy_def"
skalberg@14516
    15
skalberg@14516
    16
const_maps
skalberg@14516
    17
  "sums" > "HOL4Real.seq.sums"
skalberg@14516
    18
  "summable" > "HOL4Real.seq.summable"
skalberg@14516
    19
  "suminf" > "HOL4Real.seq.suminf"
skalberg@14516
    20
  "subseq" > "HOL4Real.seq.subseq"
skalberg@14516
    21
  "mono" > "HOL4Real.seq.mono"
skalberg@14516
    22
  "lim" > "HOL4Real.seq.lim"
obua@17694
    23
  "hol4-->" > "HOL4Real.seq.hol4-->"
skalberg@14516
    24
  "convergent" > "HOL4Real.seq.convergent"
skalberg@14516
    25
  "cauchy" > "HOL4Real.seq.cauchy"
obua@17694
    26
obua@17694
    27
const_renames
obua@17694
    28
  "-->" > "hol4-->"
skalberg@14516
    29
skalberg@14516
    30
thm_maps
skalberg@14516
    31
  "tends_num_real" > "HOL4Real.seq.tends_num_real"
skalberg@14516
    32
  "sums_def" > "HOL4Real.seq.sums_def"
skalberg@14516
    33
  "sums" > "HOL4Real.seq.sums"
skalberg@14516
    34
  "summable_def" > "HOL4Real.seq.summable_def"
skalberg@14516
    35
  "summable" > "HOL4Real.seq.summable"
skalberg@14516
    36
  "suminf_def" > "HOL4Real.seq.suminf_def"
skalberg@14516
    37
  "suminf" > "HOL4Real.seq.suminf"
skalberg@14516
    38
  "subseq_def" > "HOL4Real.seq.subseq_def"
skalberg@14516
    39
  "subseq" > "HOL4Real.seq.subseq"
skalberg@14516
    40
  "mono_def" > "HOL4Real.seq.mono_def"
skalberg@14516
    41
  "mono" > "HOL4Real.seq.mono"
skalberg@14516
    42
  "lim_def" > "HOL4Real.seq.lim_def"
skalberg@14516
    43
  "lim" > "HOL4Real.seq.lim"
obua@17694
    44
  "hol4-->_def" > "HOL4Real.seq.hol4-->_def"
skalberg@14516
    45
  "convergent_def" > "HOL4Real.seq.convergent_def"
skalberg@14516
    46
  "convergent" > "HOL4Real.seq.convergent"
skalberg@14516
    47
  "cauchy_def" > "HOL4Real.seq.cauchy_def"
skalberg@14516
    48
  "cauchy" > "HOL4Real.seq.cauchy"
skalberg@14516
    49
  "SUM_UNIQ" > "HOL4Real.seq.SUM_UNIQ"
skalberg@14516
    50
  "SUM_SUMMABLE" > "HOL4Real.seq.SUM_SUMMABLE"
skalberg@14516
    51
  "SUMMABLE_SUM" > "HOL4Real.seq.SUMMABLE_SUM"
skalberg@14516
    52
  "SUBSEQ_SUC" > "HOL4Real.seq.SUBSEQ_SUC"
skalberg@14516
    53
  "SER_ZERO" > "HOL4Real.seq.SER_ZERO"
skalberg@14516
    54
  "SER_SUB" > "HOL4Real.seq.SER_SUB"
skalberg@14516
    55
  "SER_RATIO" > "HOL4Real.seq.SER_RATIO"
skalberg@14516
    56
  "SER_POS_LT_PAIR" > "HOL4Real.seq.SER_POS_LT_PAIR"
skalberg@14516
    57
  "SER_POS_LT" > "HOL4Real.seq.SER_POS_LT"
skalberg@14516
    58
  "SER_POS_LE" > "HOL4Real.seq.SER_POS_LE"
skalberg@14516
    59
  "SER_PAIR" > "HOL4Real.seq.SER_PAIR"
skalberg@14516
    60
  "SER_OFFSET" > "HOL4Real.seq.SER_OFFSET"
skalberg@14516
    61
  "SER_NEG" > "HOL4Real.seq.SER_NEG"
skalberg@14516
    62
  "SER_LE2" > "HOL4Real.seq.SER_LE2"
skalberg@14516
    63
  "SER_LE" > "HOL4Real.seq.SER_LE"
skalberg@14516
    64
  "SER_GROUP" > "HOL4Real.seq.SER_GROUP"
skalberg@14516
    65
  "SER_COMPARA" > "HOL4Real.seq.SER_COMPARA"
skalberg@14516
    66
  "SER_COMPAR" > "HOL4Real.seq.SER_COMPAR"
skalberg@14516
    67
  "SER_CMUL" > "HOL4Real.seq.SER_CMUL"
skalberg@14516
    68
  "SER_CDIV" > "HOL4Real.seq.SER_CDIV"
skalberg@14516
    69
  "SER_CAUCHY" > "HOL4Real.seq.SER_CAUCHY"
skalberg@14516
    70
  "SER_ADD" > "HOL4Real.seq.SER_ADD"
skalberg@14516
    71
  "SER_ACONV" > "HOL4Real.seq.SER_ACONV"
skalberg@14516
    72
  "SER_ABS" > "HOL4Real.seq.SER_ABS"
skalberg@14516
    73
  "SER_0" > "HOL4Real.seq.SER_0"
skalberg@14516
    74
  "SEQ_UNIQ" > "HOL4Real.seq.SEQ_UNIQ"
skalberg@14516
    75
  "SEQ_SUC" > "HOL4Real.seq.SEQ_SUC"
skalberg@14516
    76
  "SEQ_SUBLE" > "HOL4Real.seq.SEQ_SUBLE"
skalberg@14516
    77
  "SEQ_SUB" > "HOL4Real.seq.SEQ_SUB"
skalberg@14516
    78
  "SEQ_SBOUNDED" > "HOL4Real.seq.SEQ_SBOUNDED"
skalberg@14516
    79
  "SEQ_POWER_ABS" > "HOL4Real.seq.SEQ_POWER_ABS"
skalberg@14516
    80
  "SEQ_POWER" > "HOL4Real.seq.SEQ_POWER"
skalberg@14516
    81
  "SEQ_NEG_CONV" > "HOL4Real.seq.SEQ_NEG_CONV"
skalberg@14516
    82
  "SEQ_NEG_BOUNDED" > "HOL4Real.seq.SEQ_NEG_BOUNDED"
skalberg@14516
    83
  "SEQ_NEG" > "HOL4Real.seq.SEQ_NEG"
skalberg@14516
    84
  "SEQ_MUL" > "HOL4Real.seq.SEQ_MUL"
skalberg@14516
    85
  "SEQ_MONOSUB" > "HOL4Real.seq.SEQ_MONOSUB"
skalberg@14516
    86
  "SEQ_LIM" > "HOL4Real.seq.SEQ_LIM"
skalberg@14516
    87
  "SEQ_LE" > "HOL4Real.seq.SEQ_LE"
skalberg@14516
    88
  "SEQ_INV0" > "HOL4Real.seq.SEQ_INV0"
skalberg@14516
    89
  "SEQ_INV" > "HOL4Real.seq.SEQ_INV"
skalberg@14516
    90
  "SEQ_ICONV" > "HOL4Real.seq.SEQ_ICONV"
skalberg@14516
    91
  "SEQ_DIV" > "HOL4Real.seq.SEQ_DIV"
skalberg@14516
    92
  "SEQ_DIRECT" > "HOL4Real.seq.SEQ_DIRECT"
skalberg@14516
    93
  "SEQ_CONST" > "HOL4Real.seq.SEQ_CONST"
skalberg@14516
    94
  "SEQ_CBOUNDED" > "HOL4Real.seq.SEQ_CBOUNDED"
skalberg@14516
    95
  "SEQ_CAUCHY" > "HOL4Real.seq.SEQ_CAUCHY"
skalberg@14516
    96
  "SEQ_BOUNDED_2" > "HOL4Real.seq.SEQ_BOUNDED_2"
skalberg@14516
    97
  "SEQ_BOUNDED" > "HOL4Real.seq.SEQ_BOUNDED"
skalberg@14516
    98
  "SEQ_BCONV" > "HOL4Real.seq.SEQ_BCONV"
skalberg@14516
    99
  "SEQ_ADD" > "HOL4Real.seq.SEQ_ADD"
skalberg@14516
   100
  "SEQ_ABS_IMP" > "HOL4Real.seq.SEQ_ABS_IMP"
skalberg@14516
   101
  "SEQ_ABS" > "HOL4Real.seq.SEQ_ABS"
skalberg@14516
   102
  "SEQ" > "HOL4Real.seq.SEQ"
skalberg@14516
   103
  "NEST_LEMMA_UNIQ" > "HOL4Real.seq.NEST_LEMMA_UNIQ"
skalberg@14516
   104
  "NEST_LEMMA" > "HOL4Real.seq.NEST_LEMMA"
skalberg@14516
   105
  "MONO_SUC" > "HOL4Real.seq.MONO_SUC"
skalberg@14516
   106
  "MAX_LEMMA" > "HOL4Real.seq.MAX_LEMMA"
skalberg@14516
   107
  "GP_FINITE" > "HOL4Real.seq.GP_FINITE"
skalberg@14516
   108
  "GP" > "HOL4Real.seq.GP"
skalberg@14516
   109
  "BOLZANO_LEMMA" > "HOL4Real.seq.BOLZANO_LEMMA"
skalberg@14516
   110
  "ABS_NEG_LEMMA" > "HOL4Real.seq.ABS_NEG_LEMMA"
skalberg@14516
   111
skalberg@14516
   112
end