| changeset 29667 | 53103fc8ffa3 |
| parent 28952 | 15a4b2cf8c34 |
| child 30082 | 43c5b7bfc791 |
--- a/src/HOL/RealPow.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/RealPow.thy Wed Jan 28 16:29:16 2009 +0100 @@ -58,7 +58,7 @@ lemma realpow_two_diff: "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)" apply (unfold real_diff_def) -apply (simp add: ring_simps) +apply (simp add: algebra_simps) done lemma realpow_two_disj: