--- a/src/HOL/Probability/Sigma_Algebra.thy Sun Apr 24 21:31:14 2016 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy Mon Apr 25 16:09:26 2016 +0200
@@ -846,7 +846,7 @@
proof -
from a guess Ca .. note Ca = this
from b guess Cb .. note Cb = this
- def C \<equiv> "(\<lambda>(a,b). a \<inter> b)` (Ca\<times>Cb)"
+ define C where "C = (\<lambda>(a,b). a \<inter> b)` (Ca\<times>Cb)"
show ?thesis
proof
show "disjoint C"
@@ -1971,7 +1971,7 @@
with \<open>i\<in>I\<close> * show ?thesis
by simp
next
- def P \<equiv> "\<lambda>\<mu>'. (\<forall>i\<in>I. \<mu>' (G i) = \<mu> i) \<and> measure_space \<Omega> (sigma_sets \<Omega> (G`I)) \<mu>'"
+ define P where "P \<mu>' \<longleftrightarrow> (\<forall>i\<in>I. \<mu>' (G i) = \<mu> i) \<and> measure_space \<Omega> (sigma_sets \<Omega> (G`I)) \<mu>'" for \<mu>'
assume "\<not> (\<forall>i\<in>I. \<mu> i = 0)"
moreover
have "measure_space (space M) (sets M) \<mu>'"