| changeset 35047 | 1b2bae06c796 |
| parent 35043 | 07dbdf60d5ad |
| child 35216 | 7641e8d831d2 |
--- a/src/HOL/Nat_Numeral.thy Mon Feb 08 17:12:24 2010 +0100 +++ b/src/HOL/Nat_Numeral.thy Mon Feb 08 17:12:27 2010 +0100 @@ -64,7 +64,7 @@ lemma power_even_eq: "a ^ (2*n) = (a ^ n) ^ 2" - by (subst OrderedGroup.mult_commute) (simp add: power_mult) + by (subst mult_commute) (simp add: power_mult) lemma power_odd_eq: "a ^ Suc (2*n) = a * (a ^ n) ^ 2"