summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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

3 import_segment "hol4"

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"

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"

27 const_renames

28 "-->" > "hol4-->"

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"

112 end