src/HOL/Limits.thy
changeset 56541 0e3abadbef39
parent 56536 aefb4a8da31f
child 57275 0ddb5b755cdc
     1.1 --- a/src/HOL/Limits.thy	Fri Apr 11 17:53:16 2014 +0200
     1.2 +++ b/src/HOL/Limits.thy	Fri Apr 11 22:53:33 2014 +0200
     1.3 @@ -283,8 +283,7 @@
     1.4    show ?thesis
     1.5    proof (rule ZfunI)
     1.6      fix r::real assume "0 < r"
     1.7 -    hence "0 < r / K"
     1.8 -      using K by (rule divide_pos_pos)
     1.9 +    hence "0 < r / K" using K by simp
    1.10      then have "eventually (\<lambda>x. norm (f x) < r / K) F"
    1.11        using ZfunD [OF f] by fast
    1.12      with g show "eventually (\<lambda>x. norm (g x) < r) F"
    1.13 @@ -1711,7 +1710,7 @@
    1.14      using pos_bounded by fast
    1.15    show "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
    1.16    proof (rule exI, safe)
    1.17 -    from r K show "0 < r / K" by (rule divide_pos_pos)
    1.18 +    from r K show "0 < r / K" by simp
    1.19    next
    1.20      fix x y :: 'a
    1.21      assume xy: "norm (x - y) < r / K"