Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Deriv.thy
changeset 61552 980dd46a03fb
parent 61204 3e491e34a62e
child 61609 77b453bd616f 
--- a/src/HOL/Deriv.thy	Mon Nov 02 11:56:38 2015 +0100
+++ b/src/HOL/Deriv.thy	Mon Nov 02 16:17:09 2015 +0100
@@ -745,7 +745,7 @@
   by (rule DERIV_continuous)
 
 lemma DERIV_continuous_on:
-  "(\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative D) (at x)) \<Longrightarrow> continuous_on s f"
+  "(\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative (D x)) (at x)) \<Longrightarrow> continuous_on s f"
   by (metis DERIV_continuous continuous_at_imp_continuous_on)
 
 lemma DERIV_mult':
isabelle