author  Cezary Kaliszyk <kaliszyk@in.tum.de> 
Wed, 07 Sep 2011 07:59:45 +0900  
changeset 44763  b50d5d694838 
parent 17694  b7870c2bd7df 
permissions  rwrr 
14516  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" 

17694  12 
"hol4>" > "hol4>_def" 
14516  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" 

17694  23 
"hol4>" > "HOL4Real.seq.hol4>" 
14516  24 
"convergent" > "HOL4Real.seq.convergent" 
25 
"cauchy" > "HOL4Real.seq.cauchy" 

17694  26 

27 
const_renames 

28 
">" > "hol4>" 

14516  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" 

17694  44 
"hol4>_def" > "HOL4Real.seq.hol4>_def" 
14516  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" 

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  111 

112 
end 