src/HOL/Ring_and_Field.thy
 changeset 16568 e02fe7ae212b parent 15923 01d5d0c1c078 child 16775 c1b87ef4a1c3
```     1.1 --- a/src/HOL/Ring_and_Field.thy	Sat Jun 25 12:37:07 2005 +0200
1.2 +++ b/src/HOL/Ring_and_Field.thy	Sat Jun 25 16:06:17 2005 +0200
1.3 @@ -1555,13 +1555,13 @@
1.4    have xy: "- ?x <= ?y"
1.5      apply (simp)
1.6      apply (rule_tac y="0::'a" in order_trans)
1.9      apply (simp_all add: mult_pos_le mult_neg_le)
1.12      apply (simp_all add: mult_pos_le mult_neg_le)
1.13      done
1.14    have yx: "?y <= ?x"
1.17      apply (rule_tac y=0 in order_trans)
1.20 @@ -1687,7 +1687,7 @@
1.21    have 6: "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x) <= abs (y * (A - A') + (y * A' - c') + (c'-c)) * abs x"
1.23    have 7: "(abs (y * (A - A') + (y * A' - c') + (c'-c))) * abs x <= (abs (y * (A-A') + (y*A'-c')) + abs(c'-c)) * abs x"
1.24 -    by (simp add: abs_triangle_ineq mult_right_mono)
1.25 +    by(rule abs_triangle_ineq [THEN mult_right_mono]) simp
1.26    have 8: " (abs (y * (A-A') + (y*A'-c')) + abs(c'-c)) * abs x <=  (abs (y * (A-A')) + abs (y*A'-c') + abs(c'-c)) * abs x"
1.27      by (simp add: abs_triangle_ineq mult_right_mono)
1.28    have 9: "(abs (y * (A-A')) + abs (y*A'-c') + abs(c'-c)) * abs x <= (abs y * abs (A-A') + abs (y*A'-c') + abs (c'-c)) * abs x"
1.29 @@ -1712,7 +1712,7 @@
1.30      by (simp)
1.31    show ?thesis
1.32      apply (rule_tac le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
1.33 -    apply (simp_all add: 5 14[simplified abs_of_ge_0[of y, simplified prems]])
1.34 +    apply (simp_all only: 5 14[simplified abs_of_ge_0[of y, simplified prems]])
1.35      done
1.36  qed
1.37
```