changeset 49739 | 13aa6d8268ec |
parent 48985 | 5386df44a037 |
child 51172 | 16eb76ca1e4a |
--- a/src/Doc/Codegen/Further.thy Mon Oct 08 11:37:03 2012 +0200 +++ b/src/Doc/Codegen/Further.thy Mon Oct 08 12:03:49 2012 +0200 @@ -166,7 +166,7 @@ lemma %quote powers_power: "powers xs \<circ> power x = power x \<circ> powers xs" by (induct xs) - (simp_all del: o_apply id_apply add: o_assoc [symmetric], + (simp_all del: o_apply id_apply add: comp_assoc, simp del: o_apply add: o_assoc power_commute) lemma %quote powers_rev: