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