# HG changeset patch
# User hoelzl
# Date 1298387243 -3600
# Node ID 455cbcbba8c2aad99a02f91daed33afb864c8177
# Parent  7a55699805dc4c3d5398cef0b42334cd52eb4fff
add name continuous_isCont to unnamed lemma

diff -r 7a55699805dc -r 455cbcbba8c2 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Feb 21 23:54:53 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Feb 22 16:07:23 2011 +0100
@@ -530,8 +530,8 @@
   shows "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f'') (at x) \<Longrightarrow> f' = f''"
   unfolding FDERIV_conv_has_derivative [symmetric]
   by (rule FDERIV_unique)
- 
-lemma "isCont f x = continuous (at x) f" unfolding isCont_def LIM_def
+
+lemma continuous_isCont: "isCont f x = continuous (at x) f" unfolding isCont_def LIM_def
   unfolding continuous_at Lim_at unfolding dist_nz by auto
 
 lemma frechet_derivative_unique_within_closed_interval: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"