changeset 37179 | 446cf1f997d1 |
parent 37095 | 805d18dae026 |
child 39749 | fa94799e3a3b |
--- 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"