src/HOL/Real.thy
changeset 56544 b60d5d119489
parent 56541 0e3abadbef39
child 56571 f4635657d66f
     1.1 --- a/src/HOL/Real.thy	Fri Apr 11 23:22:00 2014 +0200
     1.2 +++ b/src/HOL/Real.thy	Sat Apr 12 17:26:27 2014 +0200
     1.3 @@ -282,8 +282,7 @@
     1.4    from b i have nz: "\<forall>n\<ge>i. X n \<noteq> 0" by auto
     1.5    obtain s where s: "0 < s" and r: "r = inverse b * s * inverse b"
     1.6    proof
     1.7 -    show "0 < b * r * b"
     1.8 -      by (simp add: `0 < r` b mult_pos_pos)
     1.9 +    show "0 < b * r * b" by (simp add: `0 < r` b)
    1.10      show "r = inverse b * (b * r * b) * inverse b"
    1.11        using b by simp
    1.12    qed
    1.13 @@ -297,7 +296,7 @@
    1.14        by (simp add: inverse_diff_inverse nz * abs_mult)
    1.15      also have "\<dots> < inverse b * s * inverse b"
    1.16        by (simp add: mult_strict_mono less_imp_inverse_less
    1.17 -                    mult_pos_pos i j b * s)
    1.18 +                    i j b * s)
    1.19      finally show "\<bar>inverse (X m) - inverse (X n)\<bar> < r" unfolding r .
    1.20    qed
    1.21    thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>inverse (X m) - inverse (X n)\<bar> < r" ..
    1.22 @@ -317,7 +316,7 @@
    1.23    obtain s where s: "0 < s" and "inverse a * s * inverse b = r"
    1.24    proof
    1.25      show "0 < a * r * b"
    1.26 -      using a r b by (simp add: mult_pos_pos)
    1.27 +      using a r b by simp
    1.28      show "inverse a * (a * r * b) * inverse b = r"
    1.29        using a r b by simp
    1.30    qed
    1.31 @@ -564,7 +563,7 @@
    1.32    "positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x * y)"
    1.33  apply transfer
    1.34  apply (clarify, rename_tac a b i j)
    1.35 -apply (rule_tac x="a * b" in exI, simp add: mult_pos_pos)
    1.36 +apply (rule_tac x="a * b" in exI, simp)
    1.37  apply (rule_tac x="max i j" in exI, clarsimp)
    1.38  apply (rule mult_strict_mono, auto)
    1.39  done
    1.40 @@ -907,7 +906,7 @@
    1.41        have "\<bar>(b - a) / 2 ^ n\<bar> = \<bar>b - a\<bar> / 2 ^ n"
    1.42          by simp
    1.43        also have "\<dots> \<le> \<bar>b - a\<bar> / 2 ^ k"
    1.44 -        using n by (simp add: divide_left_mono mult_pos_pos)
    1.45 +        using n by (simp add: divide_left_mono)
    1.46        also note k
    1.47        finally show "\<bar>(b - a) / 2 ^ n\<bar> < r" .
    1.48      qed