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