1.1 --- a/src/HOL/Library/Kleene_Algebra.thy	Fri May 28 18:15:53 2010 +0200
     1.2 +++ b/src/HOL/Library/Kleene_Algebra.thy	Fri May 28 19:36:48 2010 +0100
     1.3 @@ -247,7 +247,7 @@
     1.4  by (metis add_idem2 eq_iff less_star mult_1_right star3' star_mult_idem star_unfold_left)
     1.5  
     1.6  lemma star_slide [simp]: "star (x * y) * x = x * star (y * x)"
     1.7 -by (auto simp: mult_assoc star_simulation)
     1.8 +by (metis mult_assoc star_simulation)
     1.9  
    1.10  lemma star_one':
    1.11    assumes "p * p' = 1" "p' * p = 1"