summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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.

import import_segment "hol4" def_maps "sums" > "sums_def" "summable" > "summable_def" "suminf" > "suminf_def" "subseq" > "subseq_def" "mono" > "mono_def" "lim" > "lim_def" "hol4-->" > "hol4-->_def" "convergent" > "convergent_def" "cauchy" > "cauchy_def" const_maps "sums" > "HOL4Real.seq.sums" "summable" > "HOL4Real.seq.summable" "suminf" > "HOL4Real.seq.suminf" "subseq" > "HOL4Real.seq.subseq" "mono" > "HOL4Real.seq.mono" "lim" > "HOL4Real.seq.lim" "hol4-->" > "HOL4Real.seq.hol4-->" "convergent" > "HOL4Real.seq.convergent" "cauchy" > "HOL4Real.seq.cauchy" const_renames "-->" > "hol4-->" thm_maps "tends_num_real" > "HOL4Real.seq.tends_num_real" "sums_def" > "HOL4Real.seq.sums_def" "sums" > "HOL4Real.seq.sums" "summable_def" > "HOL4Real.seq.summable_def" "summable" > "HOL4Real.seq.summable" "suminf_def" > "HOL4Real.seq.suminf_def" "suminf" > "HOL4Real.seq.suminf" "subseq_def" > "HOL4Real.seq.subseq_def" "subseq" > "HOL4Real.seq.subseq" "mono_def" > "HOL4Real.seq.mono_def" "mono" > "HOL4Real.seq.mono" "lim_def" > "HOL4Real.seq.lim_def" "lim" > "HOL4Real.seq.lim" "hol4-->_def" > "HOL4Real.seq.hol4-->_def" "convergent_def" > "HOL4Real.seq.convergent_def" "convergent" > "HOL4Real.seq.convergent" "cauchy_def" > "HOL4Real.seq.cauchy_def" "cauchy" > "HOL4Real.seq.cauchy" "SUM_UNIQ" > "HOL4Real.seq.SUM_UNIQ" "SUM_SUMMABLE" > "HOL4Real.seq.SUM_SUMMABLE" "SUMMABLE_SUM" > "HOL4Real.seq.SUMMABLE_SUM" "SUBSEQ_SUC" > "HOL4Real.seq.SUBSEQ_SUC" "SER_ZERO" > "HOL4Real.seq.SER_ZERO" "SER_SUB" > "HOL4Real.seq.SER_SUB" "SER_RATIO" > "HOL4Real.seq.SER_RATIO" "SER_POS_LT_PAIR" > "HOL4Real.seq.SER_POS_LT_PAIR" "SER_POS_LT" > "HOL4Real.seq.SER_POS_LT" "SER_POS_LE" > "HOL4Real.seq.SER_POS_LE" "SER_PAIR" > "HOL4Real.seq.SER_PAIR" "SER_OFFSET" > "HOL4Real.seq.SER_OFFSET" "SER_NEG" > "HOL4Real.seq.SER_NEG" "SER_LE2" > "HOL4Real.seq.SER_LE2" "SER_LE" > "HOL4Real.seq.SER_LE" "SER_GROUP" > "HOL4Real.seq.SER_GROUP" "SER_COMPARA" > "HOL4Real.seq.SER_COMPARA" "SER_COMPAR" > "HOL4Real.seq.SER_COMPAR" "SER_CMUL" > "HOL4Real.seq.SER_CMUL" "SER_CDIV" > "HOL4Real.seq.SER_CDIV" "SER_CAUCHY" > "HOL4Real.seq.SER_CAUCHY" "SER_ADD" > "HOL4Real.seq.SER_ADD" "SER_ACONV" > "HOL4Real.seq.SER_ACONV" "SER_ABS" > "HOL4Real.seq.SER_ABS" "SER_0" > "HOL4Real.seq.SER_0" "SEQ_UNIQ" > "HOL4Real.seq.SEQ_UNIQ" "SEQ_SUC" > "HOL4Real.seq.SEQ_SUC" "SEQ_SUBLE" > "HOL4Real.seq.SEQ_SUBLE" "SEQ_SUB" > "HOL4Real.seq.SEQ_SUB" "SEQ_SBOUNDED" > "HOL4Real.seq.SEQ_SBOUNDED" "SEQ_POWER_ABS" > "HOL4Real.seq.SEQ_POWER_ABS" "SEQ_POWER" > "HOL4Real.seq.SEQ_POWER" "SEQ_NEG_CONV" > "HOL4Real.seq.SEQ_NEG_CONV" "SEQ_NEG_BOUNDED" > "HOL4Real.seq.SEQ_NEG_BOUNDED" "SEQ_NEG" > "HOL4Real.seq.SEQ_NEG" "SEQ_MUL" > "HOL4Real.seq.SEQ_MUL" "SEQ_MONOSUB" > "HOL4Real.seq.SEQ_MONOSUB" "SEQ_LIM" > "HOL4Real.seq.SEQ_LIM" "SEQ_LE" > "HOL4Real.seq.SEQ_LE" "SEQ_INV0" > "HOL4Real.seq.SEQ_INV0" "SEQ_INV" > "HOL4Real.seq.SEQ_INV" "SEQ_ICONV" > "HOL4Real.seq.SEQ_ICONV" "SEQ_DIV" > "HOL4Real.seq.SEQ_DIV" "SEQ_DIRECT" > "HOL4Real.seq.SEQ_DIRECT" "SEQ_CONST" > "HOL4Real.seq.SEQ_CONST" "SEQ_CBOUNDED" > "HOL4Real.seq.SEQ_CBOUNDED" "SEQ_CAUCHY" > "HOL4Real.seq.SEQ_CAUCHY" "SEQ_BOUNDED_2" > "HOL4Real.seq.SEQ_BOUNDED_2" "SEQ_BOUNDED" > "HOL4Real.seq.SEQ_BOUNDED" "SEQ_BCONV" > "HOL4Real.seq.SEQ_BCONV" "SEQ_ADD" > "HOL4Real.seq.SEQ_ADD" "SEQ_ABS_IMP" > "HOL4Real.seq.SEQ_ABS_IMP" "SEQ_ABS" > "HOL4Real.seq.SEQ_ABS" "SEQ" > "HOL4Real.seq.SEQ" "NEST_LEMMA_UNIQ" > "HOL4Real.seq.NEST_LEMMA_UNIQ" "NEST_LEMMA" > "HOL4Real.seq.NEST_LEMMA" "MONO_SUC" > "HOL4Real.seq.MONO_SUC" "MAX_LEMMA" > "HOL4Real.seq.MAX_LEMMA" "GP_FINITE" > "HOL4Real.seq.GP_FINITE" "GP" > "HOL4Real.seq.GP" "BOLZANO_LEMMA" > "Deriv.lemma_BOLZANO" "ABS_NEG_LEMMA" > "Series.rabs_ratiotest_lemma" end