--- a/src/HOL/Limits.thy Fri Apr 11 17:53:16 2014 +0200
+++ b/src/HOL/Limits.thy Fri Apr 11 22:53:33 2014 +0200
@@ -283,8 +283,7 @@
show ?thesis
proof (rule ZfunI)
fix r::real assume "0 < r"
- hence "0 < r / K"
- using K by (rule divide_pos_pos)
+ hence "0 < r / K" using K by simp
then have "eventually (\<lambda>x. norm (f x) < r / K) F"
using ZfunD [OF f] by fast
with g show "eventually (\<lambda>x. norm (g x) < r) F"
@@ -1711,7 +1710,7 @@
using pos_bounded by fast
show "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
proof (rule exI, safe)
- from r K show "0 < r / K" by (rule divide_pos_pos)
+ from r K show "0 < r / K" by simp
next
fix x y :: 'a
assume xy: "norm (x - y) < r / K"