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/Borel_Space.thy
changeset 63566 e5abbdee461a
parent 63389 5d8607370faf 
--- a/src/HOL/Probability/Borel_Space.thy	Fri Jul 29 08:22:59 2016 +0200
+++ b/src/HOL/Probability/Borel_Space.thy	Fri Jul 29 20:34:07 2016 +0200
@@ -414,7 +414,7 @@
   shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow>
     (\<lambda>x. f x * indicator \<Omega> x) \<in> borel_measurable M"
   by (subst measurable_restrict_space_iff)
-     (auto simp: indicator_def if_distrib[where f="\<lambda>x. a * x" for a] cong del: if_cong)
+     (auto simp: indicator_def if_distrib[where f="\<lambda>x. a * x" for a] cong del: if_weak_cong)
 
 lemma borel_measurable_restrict_space_iff_ennreal:
   fixes f :: "'a \<Rightarrow> ennreal"
@@ -422,7 +422,7 @@
   shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow>
     (\<lambda>x. f x * indicator \<Omega> x) \<in> borel_measurable M"
   by (subst measurable_restrict_space_iff)
-     (auto simp: indicator_def if_distrib[where f="\<lambda>x. a * x" for a] cong del: if_cong)
+     (auto simp: indicator_def if_distrib[where f="\<lambda>x. a * x" for a] cong del: if_weak_cong)
 
 lemma borel_measurable_restrict_space_iff:
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
@@ -430,7 +430,8 @@
   shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow>
     (\<lambda>x. indicator \<Omega> x *\<^sub>R f x) \<in> borel_measurable M"
   by (subst measurable_restrict_space_iff)
-     (auto simp: indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a] ac_simps cong del: if_cong)
+     (auto simp: indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a] ac_simps
+       cong del: if_weak_cong)
 
 lemma cbox_borel[measurable]: "cbox a b \<in> sets borel"
   by (auto intro: borel_closed)
isabelle