src/HOL/Probability/Independent_Family.thy

     (random_variable S X \<and> random_variable T Y) \<and>
     indep_set
       (sigma_sets (space M) { X -` A \<inter> space M | A. A \<in> sets S})
       (sigma_sets (space M) { Y -` A \<inter> space M | A. A \<in> sets T})"
   unfolding indep_var_def indep_vars_def indep_set_def UNIV_bool
-  by (intro arg_cong2[where f="op \<and>"] arg_cong2[where f=indep_sets] ext)
+  by (intro arg_cong2[where f="(\<and>)"] arg_cong2[where f=indep_sets] ext)
      (auto split: bool.split)
 
 lemma (in prob_space) indep_sets2_eq:
   "indep_set A B \<longleftrightarrow> A \<subseteq> events \<and> B \<subseteq> events \<and> (\<forall>a\<in>A. \<forall>b\<in>B. prob (a \<inter> b) = prob a * prob b)"
   unfolding indep_set_def

   have  " \<P>(x in M. (X x)\<in>A \<and>  (Y x)\<in> B ) = prob ((\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M)"
     by (auto intro!: arg_cong[where f= prob])
   also have "...=  prob (X -` A \<inter> space M) * prob (Y -` B \<inter> space M)"
     by (auto intro!: indep_varD[where Ma=N and Mb=N])
   also have "... = \<P>(x in M. X x \<in> A) * \<P>(x in M. Y x \<in> B)"
-    by (auto intro!: arg_cong2[where f= "op *"] arg_cong[where f= prob])
+    by (auto intro!: arg_cong2[where f= "( * )"] arg_cong[where f= prob])
   finally show ?thesis .
 qed
 
 lemma (in prob_space)
   assumes "indep_var S X T Y"