src/HOL/BNF_Cardinal_Order_Relation.thy

   using card_of_Well_order[of A] card_of_Well_order[of B]
         ordLeq_total[of "|A|"] by blast
 qed
 
 lemma card_of_Times_Plus_distrib:
-  "|A <*> (B <+> C)| =o |A <*> B <+> A <*> C|" (is "|?RHS| =o |?LHS|")
+  "|A \<times> (B <+> C)| =o |A \<times> B <+> A \<times> C|" (is "|?RHS| =o |?LHS|")
 proof -
   let ?f = "\<lambda>(a, bc). case bc of Inl b \<Rightarrow> Inl (a, b) | Inr c \<Rightarrow> Inr (a, c)"
   have "bij_betw ?f ?RHS ?LHS" unfolding bij_betw_def inj_on_def by force
   thus ?thesis using card_of_ordIso by blast
 qed

   thus ?thesis using 1 ordLeq_ordIso_trans by blast
 qed
 
 lemma card_of_Times_ordLeq_infinite_Field:
 "\<lbrakk>\<not>finite (Field r); |A| \<le>o r; |B| \<le>o r; Card_order r\<rbrakk>
- \<Longrightarrow> |A <*> B| \<le>o r"
+ \<Longrightarrow> |A \<times> B| \<le>o r"
 by(simp add: card_of_Sigma_ordLeq_infinite_Field)
 
 lemma card_of_Times_infinite_simps:
 "\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A \<times> B| =o |A|"
 "\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |A \<times> B|"

 
 
 subsection \<open>Others\<close>
 
 lemma card_of_Func_Times:
-"|Func (A <*> B) C| =o |Func A (Func B C)|"
+"|Func (A \<times> B) C| =o |Func A (Func B C)|"
 unfolding card_of_ordIso[symmetric]
 using bij_betw_curr by blast
 
 lemma card_of_Pow_Func:
 "|Pow A| =o |Func A (UNIV::bool set)|"

     thus "h \<in> (\<lambda>f a. f a) ` {f. range f \<subseteq> B}" using f by auto
   qed(unfold Func_def fun_eq_iff, auto)
 qed
 
 lemma Func_Times_Range:
-  "|Func A (B <*> C)| =o |Func A B <*> Func A C|" (is "|?LHS| =o |?RHS|")
+  "|Func A (B \<times> C)| =o |Func A B \<times> Func A C|" (is "|?LHS| =o |?RHS|")
 proof -
   let ?F = "\<lambda>fg. (\<lambda>x. if x \<in> A then fst (fg x) else undefined,
                   \<lambda>x. if x \<in> A then snd (fg x) else undefined)"
   let ?G = "\<lambda>(f, g) x. if x \<in> A then (f x, g x) else undefined"
   have "bij_betw ?F ?LHS ?RHS" unfolding bij_betw_def inj_on_def