# HG changeset patch
# User webertj
# Date 1274623018 -3600
# Node ID 891d3333ead1f0142d6475486b4fca389bf12a54
# Parent  088ad0b57137cd6956ceca3b4fd26f8fb346d0e4
Minor proof tuning.

diff -r 088ad0b57137 -r 891d3333ead1 src/HOL/Library/Kleene_Algebra.thy
--- a/src/HOL/Library/Kleene_Algebra.thy	Sun May 23 13:00:01 2010 +0100
+++ b/src/HOL/Library/Kleene_Algebra.thy	Sun May 23 14:56:58 2010 +0100
@@ -232,7 +232,7 @@
   thus "x + star b * x * a \<le> x + star b * b * x"
     using add_mono by auto
   show "\<dots> \<le> star b * x"
-    by (metis add_supremum left_distrib less_add mult.left_neutral mult_assoc mult_right_mono star_unfold_left star_unfold_right zero_minimum)
+    by (metis add_supremum left_distrib less_add mult.left_neutral mult_assoc mult_right_mono star_unfold_right zero_minimum)
 qed
 
 lemma star_simulation [simp]: