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.7 -    apply (rule addm2)+
     1.8 +    apply (rule addm2)
     1.9      apply (simp_all add: mult_pos_le mult_neg_le)
    1.10 -    apply (rule addm)+
    1.11 +    apply (rule addm)
    1.12      apply (simp_all add: mult_pos_le mult_neg_le)
    1.13      done
    1.14    have yx: "?y <= ?x"
    1.15 -    apply (simp add: add_ac)
    1.16 +    apply (simp add:diff_def)
    1.17      apply (rule_tac y=0 in order_trans)
    1.18      apply (rule addm2, (simp add: mult_pos_neg_le mult_pos_neg2_le)+)
    1.19      apply (rule addm, (simp add: mult_pos_neg_le mult_pos_neg2_le)+)
    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.22      by (simp add: abs_le_mult)
    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