Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixes for limits
authorpaulson <lp15@cam.ac.uk>
Wed, 22 Apr 2015 12:43:06 +0100
changeset 60142 3275dddf356f
parent 60141 833adf7db7d8
child 60145 123ac30760df
fixes for limits
src/HOL/Library/BigO.thy file | annotate | diff | comparison | revisions
src/HOL/Probability/Measure_Space.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/BigO.thy	Tue Apr 21 17:19:00 2015 +0100
+++ b/src/HOL/Library/BigO.thy	Wed Apr 22 12:43:06 2015 +0100
@@ -870,7 +870,7 @@
   apply (drule bigo_LIMSEQ1)
   apply assumption
   apply (simp only: fun_diff_def)
-  apply (erule Lim_transform)
+  apply (erule Lim_transform2)
   apply assumption
   done
 
--- a/src/HOL/Probability/Measure_Space.thy	Tue Apr 21 17:19:00 2015 +0100
+++ b/src/HOL/Probability/Measure_Space.thy	Wed Apr 22 12:43:06 2015 +0100
@@ -389,7 +389,7 @@
   ultimately have "(\<lambda>i. f' (\<Union>i. A i) - f' (A i)) ----> 0"
     by (simp add: zero_ereal_def)
   then have "(\<lambda>i. f' (A i)) ----> f' (\<Union>i. A i)"
-    by (rule Lim_transform[OF tendsto_const])
+    by (rule Lim_transform2[OF tendsto_const])
   then show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
     using A by (subst (1 2) f') auto
 qed
isabelle