--- a/src/HOL/Library/Euclidean_Space.thy Fri May 29 09:58:14 2009 -0700
+++ b/src/HOL/Library/Euclidean_Space.thy Fri May 29 10:02:47 2009 -0700
@@ -697,7 +697,7 @@
qed
lemma square_continuous: "0 < (e::real) ==> \<exists>d. 0 < d \<and> (\<forall>y. abs(y - x) < d \<longrightarrow> abs(y * y - x * x) < e)"
- using isCont_power[OF isCont_ident, of 2, unfolded isCont_def LIM_def, rule_format, of e x] apply (auto simp add: power2_eq_square)
+ using isCont_power[OF isCont_ident, of 2, unfolded isCont_def LIM_eq, rule_format, of e x] apply (auto simp add: power2_eq_square)
apply (rule_tac x="s" in exI)
apply auto
apply (erule_tac x=y in allE)