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
```