src/HOL/Import/HOL/seq.imp
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Wed, 07 Sep 2011 07:59:45 +0900
changeset 44763 b50d5d694838
parent 17694 b7870c2bd7df
permissions -rw-r--r--
HOL/Import: Update HOL4 generated files to current Isabelle.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     1
import
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     2
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     3
import_segment "hol4"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     4
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     5
def_maps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     6
  "sums" > "sums_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     7
  "summable" > "summable_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     8
  "suminf" > "suminf_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     9
  "subseq" > "subseq_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    10
  "mono" > "mono_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    11
  "lim" > "lim_def"
17694
b7870c2bd7df mapped "-->" to "hol4-->"
obua
parents: 14516
diff changeset
    12
  "hol4-->" > "hol4-->_def"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    13
  "convergent" > "convergent_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    14
  "cauchy" > "cauchy_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    15
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    16
const_maps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    17
  "sums" > "HOL4Real.seq.sums"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    18
  "summable" > "HOL4Real.seq.summable"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    19
  "suminf" > "HOL4Real.seq.suminf"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    20
  "subseq" > "HOL4Real.seq.subseq"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    21
  "mono" > "HOL4Real.seq.mono"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    22
  "lim" > "HOL4Real.seq.lim"
17694
b7870c2bd7df mapped "-->" to "hol4-->"
obua
parents: 14516
diff changeset
    23
  "hol4-->" > "HOL4Real.seq.hol4-->"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    24
  "convergent" > "HOL4Real.seq.convergent"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    25
  "cauchy" > "HOL4Real.seq.cauchy"
17694
b7870c2bd7df mapped "-->" to "hol4-->"
obua
parents: 14516
diff changeset
    26
b7870c2bd7df mapped "-->" to "hol4-->"
obua
parents: 14516
diff changeset
    27
const_renames
b7870c2bd7df mapped "-->" to "hol4-->"
obua
parents: 14516
diff changeset
    28
  "-->" > "hol4-->"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    29
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    30
thm_maps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    31
  "tends_num_real" > "HOL4Real.seq.tends_num_real"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    32
  "sums_def" > "HOL4Real.seq.sums_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    33
  "sums" > "HOL4Real.seq.sums"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    34
  "summable_def" > "HOL4Real.seq.summable_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    35
  "summable" > "HOL4Real.seq.summable"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    36
  "suminf_def" > "HOL4Real.seq.suminf_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    37
  "suminf" > "HOL4Real.seq.suminf"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    38
  "subseq_def" > "HOL4Real.seq.subseq_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    39
  "subseq" > "HOL4Real.seq.subseq"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    40
  "mono_def" > "HOL4Real.seq.mono_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    41
  "mono" > "HOL4Real.seq.mono"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    42
  "lim_def" > "HOL4Real.seq.lim_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    43
  "lim" > "HOL4Real.seq.lim"
17694
b7870c2bd7df mapped "-->" to "hol4-->"
obua
parents: 14516
diff changeset
    44
  "hol4-->_def" > "HOL4Real.seq.hol4-->_def"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    45
  "convergent_def" > "HOL4Real.seq.convergent_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    46
  "convergent" > "HOL4Real.seq.convergent"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    47
  "cauchy_def" > "HOL4Real.seq.cauchy_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    48
  "cauchy" > "HOL4Real.seq.cauchy"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    49
  "SUM_UNIQ" > "HOL4Real.seq.SUM_UNIQ"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    50
  "SUM_SUMMABLE" > "HOL4Real.seq.SUM_SUMMABLE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    51
  "SUMMABLE_SUM" > "HOL4Real.seq.SUMMABLE_SUM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    52
  "SUBSEQ_SUC" > "HOL4Real.seq.SUBSEQ_SUC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    53
  "SER_ZERO" > "HOL4Real.seq.SER_ZERO"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    54
  "SER_SUB" > "HOL4Real.seq.SER_SUB"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    55
  "SER_RATIO" > "HOL4Real.seq.SER_RATIO"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    56
  "SER_POS_LT_PAIR" > "HOL4Real.seq.SER_POS_LT_PAIR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    57
  "SER_POS_LT" > "HOL4Real.seq.SER_POS_LT"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    58
  "SER_POS_LE" > "HOL4Real.seq.SER_POS_LE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    59
  "SER_PAIR" > "HOL4Real.seq.SER_PAIR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    60
  "SER_OFFSET" > "HOL4Real.seq.SER_OFFSET"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    61
  "SER_NEG" > "HOL4Real.seq.SER_NEG"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    62
  "SER_LE2" > "HOL4Real.seq.SER_LE2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    63
  "SER_LE" > "HOL4Real.seq.SER_LE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    64
  "SER_GROUP" > "HOL4Real.seq.SER_GROUP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    65
  "SER_COMPARA" > "HOL4Real.seq.SER_COMPARA"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    66
  "SER_COMPAR" > "HOL4Real.seq.SER_COMPAR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    67
  "SER_CMUL" > "HOL4Real.seq.SER_CMUL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    68
  "SER_CDIV" > "HOL4Real.seq.SER_CDIV"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    69
  "SER_CAUCHY" > "HOL4Real.seq.SER_CAUCHY"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    70
  "SER_ADD" > "HOL4Real.seq.SER_ADD"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    71
  "SER_ACONV" > "HOL4Real.seq.SER_ACONV"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    72
  "SER_ABS" > "HOL4Real.seq.SER_ABS"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    73
  "SER_0" > "HOL4Real.seq.SER_0"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    74
  "SEQ_UNIQ" > "HOL4Real.seq.SEQ_UNIQ"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    75
  "SEQ_SUC" > "HOL4Real.seq.SEQ_SUC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    76
  "SEQ_SUBLE" > "HOL4Real.seq.SEQ_SUBLE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    77
  "SEQ_SUB" > "HOL4Real.seq.SEQ_SUB"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    78
  "SEQ_SBOUNDED" > "HOL4Real.seq.SEQ_SBOUNDED"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    79
  "SEQ_POWER_ABS" > "HOL4Real.seq.SEQ_POWER_ABS"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    80
  "SEQ_POWER" > "HOL4Real.seq.SEQ_POWER"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    81
  "SEQ_NEG_CONV" > "HOL4Real.seq.SEQ_NEG_CONV"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    82
  "SEQ_NEG_BOUNDED" > "HOL4Real.seq.SEQ_NEG_BOUNDED"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    83
  "SEQ_NEG" > "HOL4Real.seq.SEQ_NEG"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    84
  "SEQ_MUL" > "HOL4Real.seq.SEQ_MUL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    85
  "SEQ_MONOSUB" > "HOL4Real.seq.SEQ_MONOSUB"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    86
  "SEQ_LIM" > "HOL4Real.seq.SEQ_LIM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    87
  "SEQ_LE" > "HOL4Real.seq.SEQ_LE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    88
  "SEQ_INV0" > "HOL4Real.seq.SEQ_INV0"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    89
  "SEQ_INV" > "HOL4Real.seq.SEQ_INV"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    90
  "SEQ_ICONV" > "HOL4Real.seq.SEQ_ICONV"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    91
  "SEQ_DIV" > "HOL4Real.seq.SEQ_DIV"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    92
  "SEQ_DIRECT" > "HOL4Real.seq.SEQ_DIRECT"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    93
  "SEQ_CONST" > "HOL4Real.seq.SEQ_CONST"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    94
  "SEQ_CBOUNDED" > "HOL4Real.seq.SEQ_CBOUNDED"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    95
  "SEQ_CAUCHY" > "HOL4Real.seq.SEQ_CAUCHY"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    96
  "SEQ_BOUNDED_2" > "HOL4Real.seq.SEQ_BOUNDED_2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    97
  "SEQ_BOUNDED" > "HOL4Real.seq.SEQ_BOUNDED"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    98
  "SEQ_BCONV" > "HOL4Real.seq.SEQ_BCONV"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    99
  "SEQ_ADD" > "HOL4Real.seq.SEQ_ADD"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   100
  "SEQ_ABS_IMP" > "HOL4Real.seq.SEQ_ABS_IMP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   101
  "SEQ_ABS" > "HOL4Real.seq.SEQ_ABS"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   102
  "SEQ" > "HOL4Real.seq.SEQ"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   103
  "NEST_LEMMA_UNIQ" > "HOL4Real.seq.NEST_LEMMA_UNIQ"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   104
  "NEST_LEMMA" > "HOL4Real.seq.NEST_LEMMA"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   105
  "MONO_SUC" > "HOL4Real.seq.MONO_SUC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   106
  "MAX_LEMMA" > "HOL4Real.seq.MAX_LEMMA"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   107
  "GP_FINITE" > "HOL4Real.seq.GP_FINITE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   108
  "GP" > "HOL4Real.seq.GP"
44763
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17694
diff changeset
   109
  "BOLZANO_LEMMA" > "Deriv.lemma_BOLZANO"
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17694
diff changeset
   110
  "ABS_NEG_LEMMA" > "Series.rabs_ratiotest_lemma"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   111
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   112
end