src/HOL/RealPow.thy
changeset 30082 43c5b7bfc791
parent 29667 53103fc8ffa3
child 30273 ecd6f0ca62ea
     1.1 --- a/src/HOL/RealPow.thy	Tue Feb 24 11:10:05 2009 -0800
     1.2 +++ b/src/HOL/RealPow.thy	Tue Feb 24 11:12:58 2009 -0800
     1.3 @@ -44,7 +44,8 @@
     1.4  by (insert power_decreasing [of 1 "Suc n" r], simp)
     1.5  
     1.6  lemma realpow_minus_mult [rule_format]:
     1.7 -     "0 < n --> (x::real) ^ (n - 1) * x = x ^ n" 
     1.8 +     "0 < n --> (x::real) ^ (n - 1) * x = x ^ n"
     1.9 +unfolding One_nat_def
    1.10  apply (simp split add: nat_diff_split)
    1.11  done
    1.12