diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Probability/Binary_Product_Measure.thy
--- a/src/HOL/Probability/Binary_Product_Measure.thy	Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Tue Sep 03 01:12:40 2013 +0200
@@ -177,9 +177,9 @@
     by (auto intro!: measurable_If simp: space_pair_measure)
 next
   case (union F)
-  moreover then have *: "\<And>x. emeasure M (Pair x -` (\<Union>i. F i)) = (\<Sum>i. ?s (F i) x)"
+  then have "\<And>x. emeasure M (Pair x -` (\<Union>i. F i)) = (\<Sum>i. ?s (F i) x)"
     by (simp add: suminf_emeasure disjoint_family_vimageI subset_eq vimage_UN sets_pair_measure[symmetric])
-  ultimately show ?case
+  with union show ?case
     unfolding sets_pair_measure[symmetric] by simp
 qed (auto simp add: if_distrib Int_def[symmetric] intro!: measurable_If)
 
@@ -515,9 +515,9 @@
   shows "(\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f (x, y) \<partial>M \<partial>M1) = integral\<^sup>P (M1 \<Otimes>\<^sub>M M) f" (is "?I f = _")
 using f proof induct
   case (cong u v)
-  moreover then have "?I u = ?I v"
+  then have "?I u = ?I v"
     by (intro positive_integral_cong) (auto simp: space_pair_measure)
-  ultimately show ?case
+  with cong show ?case
     by (simp cong: positive_integral_cong)
 qed (simp_all add: emeasure_pair_measure positive_integral_cmult positive_integral_add
                    positive_integral_monotone_convergence_SUP