fix reference to LIM_def
authorhuffman
Fri May 29 10:02:47 2009 -0700 (2009-05-29)
changeset 313405cddd98abe14
parent 31339 b4660351e8e7
child 31341 c13b080bfb34
fix reference to LIM_def
src/HOL/Library/Euclidean_Space.thy
     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Fri May 29 09:58:14 2009 -0700
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Fri May 29 10:02:47 2009 -0700
     1.3 @@ -697,7 +697,7 @@
     1.4  qed
     1.5  
     1.6  lemma square_continuous: "0 < (e::real) ==> \<exists>d. 0 < d \<and> (\<forall>y. abs(y - x) < d \<longrightarrow> abs(y * y - x * x) < e)"
     1.7 -  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)
     1.8 +  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)
     1.9    apply (rule_tac x="s" in exI)
    1.10    apply auto
    1.11    apply (erule_tac x=y in allE)