src/HOL/Import/HOL/seq.imp
changeset 44763 b50d5d694838
parent 17694 b7870c2bd7df
--- a/src/HOL/Import/HOL/seq.imp	Wed Sep 07 00:08:09 2011 +0200
+++ b/src/HOL/Import/HOL/seq.imp	Wed Sep 07 07:59:45 2011 +0900
@@ -106,7 +106,7 @@
   "MAX_LEMMA" > "HOL4Real.seq.MAX_LEMMA"
   "GP_FINITE" > "HOL4Real.seq.GP_FINITE"
   "GP" > "HOL4Real.seq.GP"
-  "BOLZANO_LEMMA" > "HOL4Real.seq.BOLZANO_LEMMA"
-  "ABS_NEG_LEMMA" > "HOL4Real.seq.ABS_NEG_LEMMA"
+  "BOLZANO_LEMMA" > "Deriv.lemma_BOLZANO"
+  "ABS_NEG_LEMMA" > "Series.rabs_ratiotest_lemma"
 
 end