src/HOL/BNF_Cardinal_Arithmetic.thy
changeset 60758 d8d85a8172b5
parent 58889 5b7a9633cfa8
child 61943 7fba644ed827
     1.1 --- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  Cardinal arithmetic as needed by bounded natural functors.
     1.5  *)
     1.6  
     1.7 -section {* Cardinal Arithmetic as Needed by Bounded Natural Functors *}
     1.8 +section \<open>Cardinal Arithmetic as Needed by Bounded Natural Functors\<close>
     1.9  
    1.10  theory BNF_Cardinal_Arithmetic
    1.11  imports BNF_Cardinal_Order_Relation
    1.12 @@ -39,7 +39,7 @@
    1.13  using card_order_on_Card_order[of UNIV r] by simp
    1.14  
    1.15  
    1.16 -subsection {* Zero *}
    1.17 +subsection \<open>Zero\<close>
    1.18  
    1.19  definition czero where
    1.20    "czero = card_of {}"
    1.21 @@ -80,7 +80,7 @@
    1.22  apply (simp only: card_of_empty3)
    1.23  done
    1.24  
    1.25 -subsection {* (In)finite cardinals *}
    1.26 +subsection \<open>(In)finite cardinals\<close>
    1.27  
    1.28  definition cinfinite where
    1.29    "cinfinite r = (\<not> finite (Field r))"
    1.30 @@ -127,7 +127,7 @@
    1.31  unfolding cinfinite_def by (auto dest: card_of_ordLeq_infinite[OF card_of_mono2])
    1.32  
    1.33  
    1.34 -subsection {* Binary sum *}
    1.35 +subsection \<open>Binary sum\<close>
    1.36  
    1.37  definition csum (infixr "+c" 65) where
    1.38    "r1 +c r2 \<equiv> |Field r1 <+> Field r2|"
    1.39 @@ -223,7 +223,7 @@
    1.40  using ordLeq_ordIso_trans[OF card_of_Un_Plus_ordLeq Plus_csum] by blast
    1.41  
    1.42  
    1.43 -subsection {* One *}
    1.44 +subsection \<open>One\<close>
    1.45  
    1.46  definition cone where
    1.47    "cone = card_of {()}"
    1.48 @@ -241,7 +241,7 @@
    1.49  unfolding cone_def by (rule Card_order_singl_ordLeq) (auto intro: czeroI)
    1.50  
    1.51  
    1.52 -subsection {* Two *}
    1.53 +subsection \<open>Two\<close>
    1.54  
    1.55  definition ctwo where
    1.56    "ctwo = |UNIV :: bool set|"
    1.57 @@ -257,7 +257,7 @@
    1.58  by (simp add: ctwo_not_czero Card_order_ctwo)
    1.59  
    1.60  
    1.61 -subsection {* Family sum *}
    1.62 +subsection \<open>Family sum\<close>
    1.63  
    1.64  definition Csum where
    1.65    "Csum r rs \<equiv> |SIGMA i : Field r. Field (rs i)|"
    1.66 @@ -278,7 +278,7 @@
    1.67  This should make cardinal reasoning more direct and natural.  *)
    1.68  
    1.69  
    1.70 -subsection {* Product *}
    1.71 +subsection \<open>Product\<close>
    1.72  
    1.73  definition cprod (infixr "*c" 80) where
    1.74    "r1 *c r2 = |Field r1 <*> Field r2|"
    1.75 @@ -360,7 +360,7 @@
    1.76  by (rule csum_absorb1') auto
    1.77  
    1.78  
    1.79 -subsection {* Exponentiation *}
    1.80 +subsection \<open>Exponentiation\<close>
    1.81  
    1.82  definition cexp (infixr "^c" 90) where
    1.83    "r1 ^c r2 \<equiv> |Func (Field r2) (Field r1)|"
    1.84 @@ -386,7 +386,7 @@
    1.85      with n have "Field r2 = {}" .
    1.86      hence "cone \<le>o r1 ^c r2" unfolding cone_def cexp_def Func_def
    1.87        by (auto intro: card_of_ordLeqI[where f="\<lambda>_ _. undefined"])
    1.88 -    thus ?thesis using `p1 ^c p2 \<le>o cone` ordLeq_transitive by auto
    1.89 +    thus ?thesis using \<open>p1 ^c p2 \<le>o cone\<close> ordLeq_transitive by auto
    1.90    next
    1.91      case False with True have "|Field (p1 ^c p2)| =o czero"
    1.92        unfolding card_of_ordIso_czero_iff_empty cexp_def Field_card_of Func_def by auto