# 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) ==> \d. 0 < d \ (\y. abs(y - x) < d \ 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)