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
```