# HG changeset patch
# User wenzelm
# Date 1451500908 -3600
# Node ID 34b51f436e929db5e8d8567248522938977a1d5c
# Parent  305baa3fc2207e53480cb33c27f1f42fefe8217f
clarified print modes;

diff -r 305baa3fc220 -r 34b51f436e92 src/HOL/Probability/Fin_Map.thy
--- 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) =
diff -r 305baa3fc220 -r 34b51f436e92 src/HOL/Probability/Finite_Product_Measure.thy
--- 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)]: