# 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 \ x + star b * b * x" using add_mono by auto show "\ \ 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]: