src/HOL/BNF_Cardinal_Arithmetic.thy

   shows "|\<Union>i \<in> I. A i| <o r"
   using card_of_UNION_ordLess_infinite_Field regularCard_stable assms cinfinite_def by blast
 
 subsection \<open>Binary sum\<close>
 
-definition csum (infixr "+c" 65) 
+definition csum (infixr \<open>+c\<close> 65) 
     where "r1 +c r2 \<equiv> |Field r1 <+> Field r2|"
 
 lemma Field_csum: "Field (r +c s) = Inl ` Field r \<union> Inr ` Field s"
   unfolding csum_def Field_card_of by auto
 

   "Csum r rs \<equiv> |SIGMA i : Field r. Field (rs i)|"
 
 (* Similar setup to the one for SIGMA from theory Big_Operators: *)
 syntax "_Csum" ::
   "pttrn => ('a * 'a) set => 'b * 'b set => (('a * 'b) * ('a * 'b)) set"
-  ("(3CSUM _:_. _)" [0, 51, 10] 10)
+  (\<open>(3CSUM _:_. _)\<close> [0, 51, 10] 10)
 
 syntax_consts
   "_Csum" == Csum
 
 translations

 This should make cardinal reasoning more direct and natural.  *)
 
 
 subsection \<open>Product\<close>
 
-definition cprod (infixr "*c" 80) where
+definition cprod (infixr \<open>*c\<close> 80) where
   "r1 *c r2 = |Field r1 \<times> Field r2|"
 
 lemma card_order_cprod:
   assumes "card_order r1" "card_order r2"
   shows "card_order (r1 *c r2)"

   qed
 qed
 
 subsection \<open>Exponentiation\<close>
 
-definition cexp (infixr "^c" 90) where
+definition cexp (infixr \<open>^c\<close> 90) where
   "r1 ^c r2 \<equiv> |Func (Field r2) (Field r1)|"
 
 lemma Card_order_cexp: "Card_order (r1 ^c r2)"
   unfolding cexp_def by (rule card_of_Card_order)