src/HOL/Ln.thy
changeset 30273 ecd6f0ca62ea
parent 29667 53103fc8ffa3
child 31338 d41a8ba25b67
     1.1 --- a/src/HOL/Ln.thy	Thu Mar 05 00:16:28 2009 +0100
     1.2 +++ b/src/HOL/Ln.thy	Wed Mar 04 17:12:23 2009 -0800
     1.3 @@ -98,7 +98,7 @@
     1.4      also have "... = x ^ 2 / 2 * (1 / 2 * (1 / 2) ^ n)"
     1.5        by auto
     1.6      also have "(1::real) / 2 * (1 / 2) ^ n = (1 / 2) ^ (Suc n)"
     1.7 -      by (rule realpow_Suc [THEN sym])
     1.8 +      by (rule power_Suc [THEN sym])
     1.9      finally show ?thesis .
    1.10    qed
    1.11  qed