# HG changeset patch
# User nipkow
# Date 1220289467 -7200
# Node ID 6ab5b4595f6438dda646430a62d506d09c07728c
# Parent  f329e59cebab185b4f72d08a4302fc4169f883f2
renamed lemma

diff -r f329e59cebab -r 6ab5b4595f64 src/HOL/NSA/HSEQ.thy
--- a/src/HOL/NSA/HSEQ.thy	Mon Sep 01 19:17:37 2008 +0200
+++ b/src/HOL/NSA/HSEQ.thy	Mon Sep 01 19:17:47 2008 +0200
@@ -202,11 +202,6 @@
 theorem LIMSEQ_NSLIMSEQ_iff: "(f ----> L) = (f ----NS> L)"
 by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ)
 
-(* Used once by Integration/Rats.thy in AFP *)
-lemma NSLIMSEQ_finite_set:
-     "!!(f::nat=>nat). \<forall>n. n \<le> f n ==> finite {n. f n \<le> u}"
-by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)
-
 subsubsection {* Derived theorems about @{term NSLIMSEQ} *}
 
 text{*We prove the NS version from the standard one, since the NS proof
diff -r f329e59cebab -r 6ab5b4595f64 src/HOL/ex/ThreeDivides.thy
--- a/src/HOL/ex/ThreeDivides.thy	Mon Sep 01 19:17:37 2008 +0200
+++ b/src/HOL/ex/ThreeDivides.thy	Mon Sep 01 19:17:47 2008 +0200
@@ -210,7 +210,7 @@
          (simp add: atLeast0LessThan)
     also have
       "\<dots> = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)"
-      by (simp add: setsum_head_upt cdef)
+      by (simp add: atLeast0LessThan[symmetric] setsum_head_upt_Suc cdef)
     also note `Suc nd = nlen m`
     finally
     show "m = (\<Sum>x<nlen m. m div 10^x mod 10 * 10^x)" .