# HG changeset patch
# User huffman
# Date 1243616567 25200
# Node ID 5cddd98abe147f835f8f0b3c268b33f0c21b35a4
# Parent  b4660351e8e7621ba83baf5a8dc530c985cd80b5
fix reference to LIM_def

diff -r b4660351e8e7 -r 5cddd98abe14 src/HOL/Library/Euclidean_Space.thy
--- 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)