--- a/src/HOL/Probability/Fin_Map.thy Wed Dec 30 18:47:13 2015 +0100
+++ b/src/HOL/Probability/Fin_Map.thy Wed Dec 30 19:41:48 2015 +0100
@@ -101,11 +101,9 @@
"Pi' I A = { P. domain P = I \<and> (\<forall>i. i \<in> I \<longrightarrow> (P)\<^sub>F i \<in> A i) } "
syntax
- "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PI' _:_./ _)" 10)
-syntax (xsymbols)
"_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi>' _\<in>_./ _)" 10)
translations
- "PI' x:A. B" == "CONST Pi' A (%x. B)"
+ "\<Pi>' x\<in>A. B" == "CONST Pi' A (\<lambda>x. B)"
subsubsection\<open>Basic Properties of @{term Pi'}\<close>
@@ -610,11 +608,9 @@
"Pi\<^sub>F I M \<equiv> PiF I M"
syntax
- "_PiF" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure" ("(3PIF _:_./ _)" 10)
-syntax (xsymbols)
"_PiF" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure" ("(3\<Pi>\<^sub>F _\<in>_./ _)" 10)
translations
- "PIF x:I. M" == "CONST PiF I (%x. M)"
+ "\<Pi>\<^sub>F x\<in>I. M" == "CONST PiF I (%x. M)"
lemma PiF_gen_subset: "{(\<Pi>' j\<in>J. X j) |X J. J \<in> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))} \<subseteq>
Pow (\<Union>J \<in> I. (\<Pi>' j\<in>J. space (M j)))"
@@ -1094,7 +1090,7 @@
qed
qed
-lemma finmap_UNIV[simp]: "(\<Union>J\<in>Collect finite. PI' j : J. UNIV) = UNIV" by auto
+lemma finmap_UNIV[simp]: "(\<Union>J\<in>Collect finite. \<Pi>' j\<in>J. UNIV) = UNIV" by auto
lemma borel_eq_PiF_borel:
shows "(borel :: ('i::countable \<Rightarrow>\<^sub>F 'a::polish_space) measure) =
--- a/src/HOL/Probability/Finite_Product_Measure.thy Wed Dec 30 18:47:13 2015 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Wed Dec 30 19:41:48 2015 +0100
@@ -169,11 +169,9 @@
"Pi\<^sub>M I M \<equiv> PiM I M"
syntax
- "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure" ("(3PIM _:_./ _)" 10)
-syntax (xsymbols)
"_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure" ("(3\<Pi>\<^sub>M _\<in>_./ _)" 10)
translations
- "PIM x:I. M" == "CONST PiM I (%x. M)"
+ "\<Pi>\<^sub>M x\<in>I. M" == "CONST PiM I (%x. M)"
lemma extend_measure_cong:
assumes "\<Omega> = \<Omega>'" "I = I'" "G = G'" "\<And>i. i \<in> I' \<Longrightarrow> \<mu> i = \<mu>' i"
@@ -507,7 +505,7 @@
lemma sets_PiM_I:
assumes "finite J" "J \<subseteq> I" "\<forall>i\<in>J. E i \<in> sets (M i)"
- shows "prod_emb I M J (PIE j:J. E j) \<in> sets (PIM i:I. M i)"
+ shows "prod_emb I M J (PIE j:J. E j) \<in> sets (\<Pi>\<^sub>M i\<in>I. M i)"
proof cases
assume "J = {}"
then have "prod_emb I M J (PIE j:J. E j) = (PIE j:I. space (M j))"
@@ -574,7 +572,7 @@
lemma sets_PiM_I_finite[measurable]:
assumes "finite I" and sets: "(\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i))"
- shows "(PIE j:I. E j) \<in> sets (PIM i:I. M i)"
+ shows "(PIE j:I. E j) \<in> sets (\<Pi>\<^sub>M i\<in>I. M i)"
using sets_PiM_I[of I I E M] sets.sets_into_space[OF sets] \<open>finite I\<close> sets by auto
lemma measurable_component_singleton[measurable (raw)]: