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/Giry_Monad.thy
changeset 69546 27dae626822b
parent 69260 0a9688695a1b
child 69861 62e47f06d22c 
--- a/src/HOL/Probability/Giry_Monad.thy	Sun Dec 30 10:34:56 2018 +0000
+++ b/src/HOL/Probability/Giry_Monad.thy	Sun Dec 30 10:34:56 2018 +0000
@@ -1763,7 +1763,7 @@
   qed
 qed
 
-lemma bind_cong_strong: "M = N \<Longrightarrow> (\<And>x. x\<in>space M =simp=> f x = g x) \<Longrightarrow> bind M f = bind N g"
+lemma bind_cong_simp: "M = N \<Longrightarrow> (\<And>x. x\<in>space M =simp=> f x = g x) \<Longrightarrow> bind M f = bind N g"
   by (auto simp: simp_implies_def intro!: bind_cong)
 
 lemma sets_bind_measurable:
isabelle