--- 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
--- 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)" .