# HG changeset patch
# User webertj
# Date 1274608501 -3600
# Node ID f1a07303d9925d2f3120d41b089ba4abe84986b0
# Parent  7753b69ea600c2e01c5b98db9c875202fc1a1633
Minor proof tuning.

diff -r 7753b69ea600 -r f1a07303d992 src/HOL/Library/Kleene_Algebra.thy
--- a/src/HOL/Library/Kleene_Algebra.thy	Sun May 23 10:38:11 2010 +0100
+++ b/src/HOL/Library/Kleene_Algebra.thy	Sun May 23 10:55:01 2010 +0100
@@ -215,8 +215,7 @@
   assumes a: "a * x \<le> x * b"
   shows "star a * x \<le> x * star b"
 proof (rule star3', rule order_trans)
-  from a have "a * x \<le> x * b" by simp
-  hence "a * x * star b \<le> x * b * star b"
+  from a have "a * x * star b \<le> x * b * star b"
     by (rule mult_right_mono) simp
   thus "x + a * (x * star b) \<le> x + x * b * star b"
     using add_left_mono by (auto simp: mult_assoc)
@@ -228,8 +227,8 @@
   assumes a: "x * a \<le> b * x"
   shows "x * star a \<le> star b * x"
 proof (rule star4', rule order_trans)
-  have "star b * x * a \<le> star b * b * x"
-    by (metis assms mult_assoc mult_mono order_refl zero_minimum)
+  from a have "star b * x * a \<le> star b * b * x"
+    by (metis mult_assoc mult_left_mono zero_minimum)
   thus "x + star b * x * a \<le> x + star b * b * x"
     using add_mono by auto
   show "\<dots> \<le> star b * x"