src/HOL/Real.thy
changeset 56541 0e3abadbef39
parent 56536 aefb4a8da31f
child 56544 b60d5d119489
     1.1 --- a/src/HOL/Real.thy	Fri Apr 11 17:53:16 2014 +0200
     1.2 +++ b/src/HOL/Real.thy	Fri Apr 11 22:53:33 2014 +0200
     1.3 @@ -110,7 +110,7 @@
     1.4      using X by fast
     1.5    obtain b where b: "0 < b" "r = a * b"
     1.6    proof
     1.7 -    show "0 < r / a" using r a by (simp add: divide_pos_pos)
     1.8 +    show "0 < r / a" using r a by simp
     1.9      show "r = a * (r / a)" using a by simp
    1.10    qed
    1.11    obtain k where k: "\<forall>n\<ge>k. \<bar>Y n\<bar> < b"
    1.12 @@ -215,8 +215,8 @@
    1.13      using cauchy_imp_bounded [OF Y] by fast
    1.14    obtain s t where s: "0 < s" and t: "0 < t" and r: "r = a * t + s * b"
    1.15    proof
    1.16 -    show "0 < v/b" using v b(1) by (rule divide_pos_pos)
    1.17 -    show "0 < u/a" using u a(1) by (rule divide_pos_pos)
    1.18 +    show "0 < v/b" using v b(1) by simp
    1.19 +    show "0 < u/a" using u a(1) by simp
    1.20      show "r = a * (u/a) + (v/b) * b"
    1.21        using a(1) b(1) `r = u + v` by simp
    1.22    qed