src/HOL/Cardinals/Bounded_Set.thy

   fix X f g
   assume "\<And>z. z \<in> set_bset X \<Longrightarrow> f z = g z"
   then show "map_bset f X = map_bset g X" by transfer force
 next
   fix f
-  show "set_bset \<circ> map_bset f = op ` f \<circ> set_bset" by (rule ext, transfer) auto
+  show "set_bset \<circ> map_bset f = (`) f \<circ> set_bset" by (rule ext, transfer) auto
 next
   fix X :: "'a set['k]"
   show "|set_bset X| \<le>o natLeq +c |UNIV :: 'k set|"
     by transfer (blast dest: ordLess_imp_ordLeq)
 next

   "rel_bset R (bset_of_option x1) (bset_of_option x2) = rel_option R x1 x2"
   unfolding bset_of_option_def bsingleton_def[abs_def]
   by transfer (auto simp: rel_set_def split: option.splits)
 
 lemma rel_bgraph[simp]:
-  "rel_bset (rel_prod (op =) R) (bgraph f1) (bgraph f2) = rel_fun (op =) (rel_option R) f1 f2"
+  "rel_bset (rel_prod (=) R) (bgraph f1) (bgraph f2) = rel_fun (=) (rel_option R) f1 f2"
   apply transfer
   apply (auto simp: rel_fun_def rel_option_iff rel_set_def split: option.splits)
   using option.collapse apply fastforce+
   done
 

   apply (rule ordLeq_ordLess_trans[OF card_of_mono1[OF subset_UNIV]])
   apply (rule ordLess_ordLeq_trans[OF card_of_set_type])
   apply (rule ordLeq_csum2[OF card_of_Card_order])
   done
 
-lift_definition bmember :: "'a \<Rightarrow> 'a set['k] \<Rightarrow> bool" is "op \<in>" .
+lift_definition bmember :: "'a \<Rightarrow> 'a set['k] \<Rightarrow> bool" is "(\<in>)" .
 
 lemma bmember_bCollect[simp]: "bmember a (bCollect P) = P a"
   by transfer simp
 
 lemma bset_eq_iff: "A = B \<longleftrightarrow> (\<forall>a. bmember a A = bmember a B)"