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/Probability/Distributions.thy
changeset 59587 8ea7b22525cb
parent 59000 6eb0725503fc
child 59730 b7c394c7a619 
--- a/src/HOL/Probability/Distributions.thy	Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Probability/Distributions.thy	Wed Mar 04 23:31:04 2015 +0100
@@ -119,7 +119,7 @@
     apply (intro nn_integral_LIMSEQ)
     apply (auto simp: incseq_def le_fun_def eventually_sequentially
                 split: split_indicator intro!: Lim_eventually)
-    apply (metis natceiling_le_eq)
+    apply (metis nat_ceiling_le_eq)
     done
 
   have "((\<lambda>x. (1 - (\<Sum>n\<le>k. (x ^ n / exp x) / real (fact n))) * fact k) ---> (1 - (\<Sum>n\<le>k. 0 / real (fact n))) * fact k) at_top"
isabelle