changeset 63648 | f9f3006a5579 |
parent 63417 | c184ec919c70 |
child 63654 | f90e3926e627 |
--- a/src/HOL/Power.thy Tue Aug 09 23:29:54 2016 +0200 +++ b/src/HOL/Power.thy Wed Aug 10 09:33:54 2016 +0200 @@ -112,7 +112,7 @@ lemma power_minus_mult: "0 < n \<Longrightarrow> a ^ (n - 1) * a = a ^ n" - by (simp add: power_commutes split add: nat_diff_split) + by (simp add: power_commutes split: nat_diff_split) end