src/HOL/BNF_Def.thy

   by simp
 
 lemma case_sum_o_inj: "case_sum f g \<circ> Inl = f" "case_sum f g \<circ> Inr = g"
   by auto
 
-lemma map_sum_o_inj: "map_sum f g o Inl = Inl o f" "map_sum f g o Inr = Inr o g"
+lemma map_sum_o_inj: "map_sum f g \<circ> Inl = Inl \<circ> f" "map_sum f g \<circ> Inr = Inr \<circ> g"
   by auto
 
 lemma card_order_csum_cone_cexp_def:
   "card_order r \<Longrightarrow> ( |A1| +c cone) ^c r = |Func UNIV (Inl ` A1 \<union> {Inr ()})|"
   unfolding cexp_def cone_def Field_csum Field_card_of by (auto dest: Field_card_order)

   unfolding eq_onp_def by auto
 
 lemma eq_onp_True: "eq_onp (\<lambda>_. True) = (op =)"
   unfolding eq_onp_def by simp
 
-lemma Ball_image_comp: "Ball (f ` A) g = Ball A (g o f)"
+lemma Ball_image_comp: "Ball (f ` A) g = Ball A (g \<circ> f)"
   by auto
 
 lemma rel_fun_Collect_case_prodD:
-  "rel_fun A B f g \<Longrightarrow> X \<subseteq> Collect (case_prod A) \<Longrightarrow> x \<in> X \<Longrightarrow> B ((f o fst) x) ((g o snd) x)"
+  "rel_fun A B f g \<Longrightarrow> X \<subseteq> Collect (case_prod A) \<Longrightarrow> x \<in> X \<Longrightarrow> B ((f \<circ> fst) x) ((g \<circ> snd) x)"
   unfolding rel_fun_def by auto
 
 lemma eq_onp_mono_iff: "eq_onp P \<le> eq_onp Q \<longleftrightarrow> P \<le> Q"
   unfolding eq_onp_def by auto