# HG changeset patch
# User webertj
# Date 1275071808 -3600
# Node ID 446cf1f997d19a6d89b9d57ec6c32ae8da0c6125
# Parent  ece850d911a5a2c1bb86e2f56629e2d478d961a4
Got rid of a warning about duplicate rewrite rules.

diff -r ece850d911a5 -r 446cf1f997d1 src/HOL/Library/Kleene_Algebra.thy
--- a/src/HOL/Library/Kleene_Algebra.thy	Fri May 28 18:15:53 2010 +0200
+++ b/src/HOL/Library/Kleene_Algebra.thy	Fri May 28 19:36:48 2010 +0100
@@ -247,7 +247,7 @@
 by (metis add_idem2 eq_iff less_star mult_1_right star3' star_mult_idem star_unfold_left)
 
 lemma star_slide [simp]: "star (x * y) * x = x * star (y * x)"
-by (auto simp: mult_assoc star_simulation)
+by (metis mult_assoc star_simulation)
 
 lemma star_one':
   assumes "p * p' = 1" "p' * p = 1"