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