src/HOL/Probability/Sigma_Algebra.thy

   using algebra.is_sigma_algebra[OF algebra_single_set[OF `X \<subseteq> S`]] by simp
 
 subsection {* Binary Unions *}
 
 definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"
-  where "binary a b =  (\<lambda>\<^isup>x. b)(0 := a)"
+  where "binary a b =  (\<lambda>x. b)(0 := a)"
 
 lemma range_binary_eq: "range(binary a b) = {a,b}"
   by (auto simp add: binary_def)
 
 lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)"

 qed
 
 subsection {* A Two-Element Series *}
 
 definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set "
-  where "binaryset A B = (\<lambda>\<^isup>x. {})(0 := A, Suc 0 := B)"
+  where "binaryset A B = (\<lambda>x. {})(0 := A, Suc 0 := B)"
 
 lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}"
   apply (simp add: binaryset_def)
   apply (rule set_eqI)
   apply (auto simp add: image_iff)