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/Multivariate_Analysis/Derivative.thy
changeset 44907 93943da0a010
parent 44890 22f665a2e91c
child 45031 9583f2b56f85 
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Sep 12 11:39:29 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Sep 12 11:54:20 2011 -0700
@@ -1466,7 +1466,7 @@
     apply(rule,rule,rule g[rule_format],assumption)
   proof fix x assume "x\<in>s"
     have lem3:"\<forall>u. ((\<lambda>n. f' n x u) ---> g' x u) sequentially"
-      unfolding Lim_sequentially
+      unfolding LIMSEQ_def
     proof(rule,rule,rule)
       fix u and e::real assume "e>0"
       show "\<exists>N. \<forall>n\<ge>N. dist (f' n x u) (g' x u) < e"
isabelle