diff -r f869bb857425 -r 314a88278715 src/HOL/Matrix/LP.thy
--- a/src/HOL/Matrix/LP.thy	Mon Jul 19 12:17:38 2010 +0200
+++ b/src/HOL/Matrix/LP.thy	Mon Jul 19 16:09:43 2010 +0200
@@ -6,6 +6,15 @@
 imports Main Lattice_Algebras
 begin
 
+lemma le_add_right_mono: 
+  assumes 
+  "a <= b + (c::'a::ordered_ab_group_add)"
+  "c <= d"    
+  shows "a <= b + d"
+  apply (rule_tac order_trans[where y = "b+c"])
+  apply (simp_all add: prems)
+  done
+
 lemma linprog_dual_estimate:
   assumes
   "A * x \<le> (b::'a::lattice_ring)"
@@ -49,8 +58,8 @@
     done    
   from 6 7 8 9 12 13 r have 14:" abs((y * (A - A') + (y * A' - c') + (c'-c)) * x) <=(abs y * \<delta>A + abs (y*A'-c') + \<delta>c) * r"     
     by (simp)
-  show ?thesis 
-    apply (rule_tac le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
+  show ?thesis
+    apply (rule le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
     apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified prems]])
     done
 qed
@@ -138,9 +147,9 @@
   then have "c * x <= y * b - (y * A - c) * x" by (simp add: le_diff_eq)
   then have cx: "c * x <= y * b + (c - y * A) * x" by (simp add: algebra_simps)
   have s2: "c - y * A <= c2 - y * A1"
-    by (simp add: diff_def prems add_mono mult_left_mono)
+    by (simp add: diff_minus prems add_mono mult_left_mono)
   have s1: "c1 - y * A2 <= c - y * A"
-    by (simp add: diff_def prems add_mono mult_left_mono)
+    by (simp add: diff_minus prems add_mono mult_left_mono)
   have prts: "(c - y * A) * x <= ?C"
     apply (simp add: Let_def)
     apply (rule mult_le_prts)