src/HOL/Import/HOL/seq.imp
changeset 44763 b50d5d694838
parent 17694 b7870c2bd7df
equal deleted inserted replaced
44762:8f9d09241a68 44763:b50d5d694838
   104   "NEST_LEMMA" > "HOL4Real.seq.NEST_LEMMA"
   104   "NEST_LEMMA" > "HOL4Real.seq.NEST_LEMMA"
   105   "MONO_SUC" > "HOL4Real.seq.MONO_SUC"
   105   "MONO_SUC" > "HOL4Real.seq.MONO_SUC"
   106   "MAX_LEMMA" > "HOL4Real.seq.MAX_LEMMA"
   106   "MAX_LEMMA" > "HOL4Real.seq.MAX_LEMMA"
   107   "GP_FINITE" > "HOL4Real.seq.GP_FINITE"
   107   "GP_FINITE" > "HOL4Real.seq.GP_FINITE"
   108   "GP" > "HOL4Real.seq.GP"
   108   "GP" > "HOL4Real.seq.GP"
   109   "BOLZANO_LEMMA" > "HOL4Real.seq.BOLZANO_LEMMA"
   109   "BOLZANO_LEMMA" > "Deriv.lemma_BOLZANO"
   110   "ABS_NEG_LEMMA" > "HOL4Real.seq.ABS_NEG_LEMMA"
   110   "ABS_NEG_LEMMA" > "Series.rabs_ratiotest_lemma"
   111 
   111 
   112 end
   112 end