diff -r 9b6a0fb85fa3 -r c3658c18b7bc src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Tue Oct 13 09:21:15 2015 +0200
@@ -12,7 +12,7 @@
by (auto simp: Bex_def PiE_iff Ball_def dest!: choice_iff'[THEN iffD1])
(force intro: exI[of _ "restrict f I" for f])
-lemma split_const: "(\(i, j). c) = (\_. c)"
+lemma case_prod_const: "(\(i, j). c) = (\_. c)"
by auto
subsubsection {* More about Function restricted by @{const extensional} *}
@@ -1110,7 +1110,7 @@
qed (simp add: space_PiM)
lemma (in product_sigma_finite) product_nn_integral_pair:
- assumes [measurable]: "split f \ borel_measurable (M x \\<^sub>M M y)"
+ assumes [measurable]: "case_prod f \ borel_measurable (M x \\<^sub>M M y)"
assumes xy: "x \ y"
shows "(\\<^sup>+\. f (\ x) (\ y) \PiM {x, y} M) = (\\<^sup>+z. f (fst z) (snd z) \(M x \\<^sub>M M y))"
proof-