src/HOL/Nat.thy
changeset 60758 d8d85a8172b5
parent 60636 ee18efe9b246
child 61070 b72a990adfe2
     1.1 --- a/src/HOL/Nat.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Nat.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  and * (for div and mod, see theory Divides).
     1.5  *)
     1.6  
     1.7 -section {* Natural numbers *}
     1.8 +section \<open>Natural numbers\<close>
     1.9  
    1.10  theory Nat
    1.11  imports Inductive Typedef Fun Fields
    1.12 @@ -18,18 +18,18 @@
    1.13  ML_file "~~/src/Provers/Arith/fast_lin_arith.ML"
    1.14  
    1.15  
    1.16 -subsection {* Type @{text ind} *}
    1.17 +subsection \<open>Type @{text ind}\<close>
    1.18  
    1.19  typedecl ind
    1.20  
    1.21  axiomatization Zero_Rep :: ind and Suc_Rep :: "ind => ind" where
    1.22 -  -- {* the axiom of infinity in 2 parts *}
    1.23 +  -- \<open>the axiom of infinity in 2 parts\<close>
    1.24    Suc_Rep_inject:       "Suc_Rep x = Suc_Rep y ==> x = y" and
    1.25    Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
    1.26  
    1.27 -subsection {* Type nat *}
    1.28 -
    1.29 -text {* Type definition *}
    1.30 +subsection \<open>Type nat\<close>
    1.31 +
    1.32 +text \<open>Type definition\<close>
    1.33  
    1.34  inductive Nat :: "ind \<Rightarrow> bool" where
    1.35    Zero_RepI: "Nat Zero_Rep"
    1.36 @@ -79,7 +79,7 @@
    1.37    shows "P n"
    1.38  using assms
    1.39  apply (unfold Zero_nat_def Suc_def)
    1.40 -apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
    1.41 +apply (rule Rep_Nat_inverse [THEN subst]) -- \<open>types force good instantiation\<close>
    1.42  apply (erule Nat_Rep_Nat [THEN Nat.induct])
    1.43  apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
    1.44  done
    1.45 @@ -96,8 +96,8 @@
    1.46    apply (simp only: Suc_not_Zero)
    1.47    done
    1.48  
    1.49 --- {* Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}. *}
    1.50 -setup {* Sign.mandatory_path "old" *}
    1.51 +-- \<open>Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}.\<close>
    1.52 +setup \<open>Sign.mandatory_path "old"\<close>
    1.53  
    1.54  old_rep_datatype "0 \<Colon> nat" Suc
    1.55    apply (erule nat_induct0, assumption)
    1.56 @@ -105,10 +105,10 @@
    1.57  apply (rule nat.distinct(1))
    1.58  done
    1.59  
    1.60 -setup {* Sign.parent_path *}
    1.61 -
    1.62 --- {* But erase the prefix for properties that are not generated by @{text free_constructors}. *}
    1.63 -setup {* Sign.mandatory_path "nat" *}
    1.64 +setup \<open>Sign.parent_path\<close>
    1.65 +
    1.66 +-- \<open>But erase the prefix for properties that are not generated by @{text free_constructors}.\<close>
    1.67 +setup \<open>Sign.mandatory_path "nat"\<close>
    1.68  
    1.69  declare
    1.70    old.nat.inject[iff del]
    1.71 @@ -119,14 +119,14 @@
    1.72  lemmas rec = old.nat.rec
    1.73  lemmas simps = nat.inject nat.distinct nat.case nat.rec
    1.74  
    1.75 -setup {* Sign.parent_path *}
    1.76 +setup \<open>Sign.parent_path\<close>
    1.77  
    1.78  abbreviation rec_nat :: "'a \<Rightarrow> (nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a" where
    1.79    "rec_nat \<equiv> old.rec_nat"
    1.80  
    1.81  declare nat.sel[code del]
    1.82  
    1.83 -hide_const (open) Nat.pred -- {* hide everything related to the selector *}
    1.84 +hide_const (open) Nat.pred -- \<open>hide everything related to the selector\<close>
    1.85  hide_fact
    1.86    nat.case_eq_if
    1.87    nat.collapse
    1.88 @@ -137,12 +137,12 @@
    1.89    nat.split_sel_asm
    1.90  
    1.91  lemma nat_exhaust [case_names 0 Suc, cases type: nat]:
    1.92 -  -- {* for backward compatibility -- names of variables differ *}
    1.93 +  -- \<open>for backward compatibility -- names of variables differ\<close>
    1.94    "(y = 0 \<Longrightarrow> P) \<Longrightarrow> (\<And>nat. y = Suc nat \<Longrightarrow> P) \<Longrightarrow> P"
    1.95  by (rule old.nat.exhaust)
    1.96  
    1.97  lemma nat_induct [case_names 0 Suc, induct type: nat]:
    1.98 -  -- {* for backward compatibility -- names of variables differ *}
    1.99 +  -- \<open>for backward compatibility -- names of variables differ\<close>
   1.100    fixes n
   1.101    assumes "P 0" and "\<And>n. P n \<Longrightarrow> P (Suc n)"
   1.102    shows "P n"
   1.103 @@ -152,7 +152,7 @@
   1.104    nat_exhaust
   1.105    nat_induct0
   1.106  
   1.107 -ML {*
   1.108 +ML \<open>
   1.109  val nat_basic_lfp_sugar =
   1.110    let
   1.111      val ctr_sugar = the (Ctr_Sugar.ctr_sugar_of_global @{theory} @{type_name nat});
   1.112 @@ -162,9 +162,9 @@
   1.113      {T = HOLogic.natT, fp_res_index = 0, C = C, fun_arg_Tsss = [[], [[HOLogic.natT, C]]],
   1.114       ctr_sugar = ctr_sugar, recx = recx, rec_thms = @{thms nat.rec}}
   1.115    end;
   1.116 -*}
   1.117 -
   1.118 -setup {*
   1.119 +\<close>
   1.120 +
   1.121 +setup \<open>
   1.122  let
   1.123    fun basic_lfp_sugars_of _ [@{typ nat}] _ _ ctxt =
   1.124        ([], [0], [nat_basic_lfp_sugar], [], [], TrueI (*dummy*), [], false, ctxt)
   1.125 @@ -175,9 +175,9 @@
   1.126      {nested_simps = [], is_new_datatype = K (K true), basic_lfp_sugars_of = basic_lfp_sugars_of,
   1.127       rewrite_nested_rec_call = NONE}
   1.128  end
   1.129 -*}
   1.130 -
   1.131 -text {* Injectiveness and distinctness lemmas *}
   1.132 +\<close>
   1.133 +
   1.134 +text \<open>Injectiveness and distinctness lemmas\<close>
   1.135  
   1.136  lemma inj_Suc[simp]: "inj_on Suc N"
   1.137    by (simp add: inj_on_def)
   1.138 @@ -197,8 +197,8 @@
   1.139  lemma Suc_n_not_n: "Suc n \<noteq> n"
   1.140  by (rule not_sym, rule n_not_Suc_n)
   1.141  
   1.142 -text {* A special form of induction for reasoning
   1.143 -  about @{term "m < n"} and @{term "m - n"} *}
   1.144 +text \<open>A special form of induction for reasoning
   1.145 +  about @{term "m < n"} and @{term "m - n"}\<close>
   1.146  
   1.147  lemma diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
   1.148      (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"
   1.149 @@ -210,7 +210,7 @@
   1.150    done
   1.151  
   1.152  
   1.153 -subsection {* Arithmetic operators *}
   1.154 +subsection \<open>Arithmetic operators\<close>
   1.155  
   1.156  instantiation nat :: comm_monoid_diff
   1.157  begin
   1.158 @@ -290,7 +290,7 @@
   1.159  
   1.160  end
   1.161  
   1.162 -text {* Difference distributes over multiplication *}
   1.163 +text \<open>Difference distributes over multiplication\<close>
   1.164  
   1.165  lemma diff_mult_distrib:
   1.166    "((m::nat) - n) * k = (m * k) - (n * k)"
   1.167 @@ -301,7 +301,7 @@
   1.168    by (fact right_diff_distrib')
   1.169  
   1.170  
   1.171 -subsubsection {* Addition *}
   1.172 +subsubsection \<open>Addition\<close>
   1.173  
   1.174  lemma nat_add_left_cancel:
   1.175    fixes k m n :: nat
   1.176 @@ -313,7 +313,7 @@
   1.177    shows "m + k = n + k \<longleftrightarrow> m = n"
   1.178    by (fact add_right_cancel)
   1.179  
   1.180 -text {* Reasoning about @{text "m + 0 = 0"}, etc. *}
   1.181 +text \<open>Reasoning about @{text "m + 0 = 0"}, etc.\<close>
   1.182  
   1.183  lemma add_is_0 [iff]:
   1.184    fixes m n :: nat
   1.185 @@ -347,7 +347,7 @@
   1.186    unfolding One_nat_def by simp
   1.187  
   1.188  
   1.189 -subsubsection {* Difference *}
   1.190 +subsubsection \<open>Difference\<close>
   1.191  
   1.192  lemma diff_self_eq_0 [simp]: "(m\<Colon>nat) - m = 0"
   1.193    by (fact diff_cancel)
   1.194 @@ -379,7 +379,7 @@
   1.195  lemma diff_Suc_1 [simp]: "Suc n - 1 = n"
   1.196    unfolding One_nat_def by simp
   1.197  
   1.198 -subsubsection {* Multiplication *}
   1.199 +subsubsection \<open>Multiplication\<close>
   1.200  
   1.201  lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
   1.202    by (fact distrib_left)
   1.203 @@ -427,9 +427,9 @@
   1.204    by (subst mult_cancel1) simp
   1.205  
   1.206  
   1.207 -subsection {* Orders on @{typ nat} *}
   1.208 -
   1.209 -subsubsection {* Operation definition *}
   1.210 +subsection \<open>Orders on @{typ nat}\<close>
   1.211 +
   1.212 +subsubsection \<open>Operation definition\<close>
   1.213  
   1.214  instantiation nat :: linorder
   1.215  begin
   1.216 @@ -532,7 +532,7 @@
   1.217    by default (auto intro: less_Suc_eq_le [THEN iffD2])
   1.218  
   1.219  
   1.220 -subsubsection {* Introduction properties *}
   1.221 +subsubsection \<open>Introduction properties\<close>
   1.222  
   1.223  lemma lessI [iff]: "n < Suc n"
   1.224    by (simp add: less_Suc_eq_le)
   1.225 @@ -541,7 +541,7 @@
   1.226    by (simp add: less_Suc_eq_le)
   1.227  
   1.228  
   1.229 -subsubsection {* Elimination properties *}
   1.230 +subsubsection \<open>Elimination properties\<close>
   1.231  
   1.232  lemma less_not_refl: "~ n < (n::nat)"
   1.233    by (rule order_less_irrefl)
   1.234 @@ -570,7 +570,7 @@
   1.235  lemma Suc_mono: "m < n ==> Suc m < Suc n"
   1.236    by simp
   1.237  
   1.238 -text {* "Less than" is antisymmetric, sort of *}
   1.239 +text \<open>"Less than" is antisymmetric, sort of\<close>
   1.240  lemma less_antisym: "\<lbrakk> \<not> n < m; n < Suc m \<rbrakk> \<Longrightarrow> m = n"
   1.241    unfolding not_less less_Suc_eq_le by (rule antisym)
   1.242  
   1.243 @@ -588,7 +588,7 @@
   1.244    done
   1.245  
   1.246  
   1.247 -subsubsection {* Inductive (?) properties *}
   1.248 +subsubsection \<open>Inductive (?) properties\<close>
   1.249  
   1.250  lemma Suc_lessI: "m < n ==> Suc m \<noteq> n ==> Suc m < n"
   1.251    unfolding less_eq_Suc_le [of m] le_less by simp
   1.252 @@ -630,14 +630,14 @@
   1.253    apply (blast dest: Suc_lessD)
   1.254    done
   1.255  
   1.256 -text {* Can be used with @{text less_Suc_eq} to get @{term "n = m | n < m"} *}
   1.257 +text \<open>Can be used with @{text less_Suc_eq} to get @{term "n = m | n < m"}\<close>
   1.258  lemma not_less_eq: "\<not> m < n \<longleftrightarrow> n < Suc m"
   1.259    unfolding not_less less_Suc_eq_le ..
   1.260  
   1.261  lemma not_less_eq_eq: "\<not> m \<le> n \<longleftrightarrow> Suc n \<le> m"
   1.262    unfolding not_le Suc_le_eq ..
   1.263  
   1.264 -text {* Properties of "less than or equal" *}
   1.265 +text \<open>Properties of "less than or equal"\<close>
   1.266  
   1.267  lemma le_imp_less_Suc: "m \<le> n ==> m < Suc n"
   1.268    unfolding less_Suc_eq_le .
   1.269 @@ -654,18 +654,18 @@
   1.270  lemma Suc_leI: "m < n ==> Suc(m) \<le> n"
   1.271    unfolding Suc_le_eq .
   1.272  
   1.273 -text {* Stronger version of @{text Suc_leD} *}
   1.274 +text \<open>Stronger version of @{text Suc_leD}\<close>
   1.275  lemma Suc_le_lessD: "Suc m \<le> n ==> m < n"
   1.276    unfolding Suc_le_eq .
   1.277  
   1.278  lemma less_imp_le_nat: "m < n ==> m \<le> (n::nat)"
   1.279    unfolding less_eq_Suc_le by (rule Suc_leD)
   1.280  
   1.281 -text {* For instance, @{text "(Suc m < Suc n) = (Suc m \<le> n) = (m < n)"} *}
   1.282 +text \<open>For instance, @{text "(Suc m < Suc n) = (Suc m \<le> n) = (m < n)"}\<close>
   1.283  lemmas le_simps = less_imp_le_nat less_Suc_eq_le Suc_le_eq
   1.284  
   1.285  
   1.286 -text {* Equivalence of @{term "m \<le> n"} and @{term "m < n | m = n"} *}
   1.287 +text \<open>Equivalence of @{term "m \<le> n"} and @{term "m < n | m = n"}\<close>
   1.288  
   1.289  lemma less_or_eq_imp_le: "m < n | m = n ==> m \<le> (n::nat)"
   1.290    unfolding le_less .
   1.291 @@ -673,7 +673,7 @@
   1.292  lemma le_eq_less_or_eq: "(m \<le> (n::nat)) = (m < n | m=n)"
   1.293    by (rule le_less)
   1.294  
   1.295 -text {* Useful with @{text blast}. *}
   1.296 +text \<open>Useful with @{text blast}.\<close>
   1.297  lemma eq_imp_le: "(m::nat) = n ==> m \<le> n"
   1.298    by auto
   1.299  
   1.300 @@ -717,7 +717,7 @@
   1.301  lemma neq0_conv[iff]: fixes n :: nat shows "(n \<noteq> 0) = (0 < n)"
   1.302  by (cases n) simp_all
   1.303  
   1.304 -text {* This theorem is useful with @{text blast} *}
   1.305 +text \<open>This theorem is useful with @{text blast}\<close>
   1.306  lemma gr0I: "((n::nat) = 0 ==> False) ==> 0 < n"
   1.307  by (rule neq0_conv[THEN iffD1], iprover)
   1.308  
   1.309 @@ -730,12 +730,12 @@
   1.310  lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)"
   1.311  by (induct m') simp_all
   1.312  
   1.313 -text {* Useful in certain inductive arguments *}
   1.314 +text \<open>Useful in certain inductive arguments\<close>
   1.315  lemma less_Suc_eq_0_disj: "(m < Suc n) = (m = 0 | (\<exists>j. m = Suc j & j < n))"
   1.316  by (cases m) simp_all
   1.317  
   1.318  
   1.319 -subsubsection {* Monotonicity of Addition *}
   1.320 +subsubsection \<open>Monotonicity of Addition\<close>
   1.321  
   1.322  lemma Suc_pred [simp]: "n>0 ==> Suc (n - Suc 0) = n"
   1.323  by (simp add: diff_Suc split: nat.split)
   1.324 @@ -752,17 +752,17 @@
   1.325  lemma add_gr_0 [iff]: "!!m::nat. (m + n > 0) = (m>0 | n>0)"
   1.326  by(auto dest:gr0_implies_Suc)
   1.327  
   1.328 -text {* strict, in 1st argument *}
   1.329 +text \<open>strict, in 1st argument\<close>
   1.330  lemma add_less_mono1: "i < j ==> i + k < j + (k::nat)"
   1.331  by (induct k) simp_all
   1.332  
   1.333 -text {* strict, in both arguments *}
   1.334 +text \<open>strict, in both arguments\<close>
   1.335  lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)"
   1.336    apply (rule add_less_mono1 [THEN less_trans], assumption+)
   1.337    apply (induct j, simp_all)
   1.338    done
   1.339  
   1.340 -text {* Deleted @{text less_natE}; use @{text "less_imp_Suc_add RS exE"} *}
   1.341 +text \<open>Deleted @{text less_natE}; use @{text "less_imp_Suc_add RS exE"}\<close>
   1.342  lemma less_imp_Suc_add: "m < n ==> (\<exists>k. n = Suc (m + k))"
   1.343    apply (induct n)
   1.344    apply (simp_all add: order_le_less)
   1.345 @@ -773,20 +773,20 @@
   1.346  lemma le_Suc_ex: "(k::nat) \<le> l \<Longrightarrow> (\<exists>n. l = k + n)"
   1.347    by (auto simp: less_Suc_eq_le[symmetric] dest: less_imp_Suc_add)
   1.348  
   1.349 -text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *}
   1.350 +text \<open>strict, in 1st argument; proof is by induction on @{text "k > 0"}\<close>
   1.351  lemma mult_less_mono2: "(i::nat) < j ==> 0<k ==> k * i < k * j"
   1.352  apply(auto simp: gr0_conv_Suc)
   1.353  apply (induct_tac m)
   1.354  apply (simp_all add: add_less_mono)
   1.355  done
   1.356  
   1.357 -text {* Addition is the inverse of subtraction:
   1.358 -  if @{term "n \<le> m"} then @{term "n + (m - n) = m"}. *}
   1.359 +text \<open>Addition is the inverse of subtraction:
   1.360 +  if @{term "n \<le> m"} then @{term "n + (m - n) = m"}.\<close>
   1.361  lemma add_diff_inverse_nat: "~  m < n ==> n + (m - n) = (m::nat)"
   1.362  by (induct m n rule: diff_induct) simp_all
   1.363  
   1.364  
   1.365 -text{*The naturals form an ordered @{text semidom}*}
   1.366 +text\<open>The naturals form an ordered @{text semidom}\<close>
   1.367  instance nat :: linordered_semidom
   1.368  proof
   1.369    show "0 < (1::nat)" by simp
   1.370 @@ -798,7 +798,7 @@
   1.371  qed 
   1.372  
   1.373  
   1.374 -subsubsection {* @{term min} and @{term max} *}
   1.375 +subsubsection \<open>@{term min} and @{term max}\<close>
   1.376  
   1.377  lemma mono_Suc: "mono Suc"
   1.378  by (rule monoI) simp
   1.379 @@ -868,9 +868,9 @@
   1.380    by (simp add: max_def not_le) (auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans)
   1.381  
   1.382  
   1.383 -subsubsection {* Additional theorems about @{term "op \<le>"} *}
   1.384 -
   1.385 -text {* Complete induction, aka course-of-values induction *}
   1.386 +subsubsection \<open>Additional theorems about @{term "op \<le>"}\<close>
   1.387 +
   1.388 +text \<open>Complete induction, aka course-of-values induction\<close>
   1.389  
   1.390  instance nat :: wellorder proof
   1.391    fix P and n :: nat
   1.392 @@ -947,7 +947,7 @@
   1.393    shows "P a"
   1.394  by (induct m\<equiv>"f a" arbitrary: a rule: less_induct) (auto intro: step)
   1.395  
   1.396 -text {* old style induction rules: *}
   1.397 +text \<open>old style induction rules:\<close>
   1.398  lemma measure_induct:
   1.399    fixes f :: "'a \<Rightarrow> nat"
   1.400    shows "(\<And>x. \<forall>y. f y < f x \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a"
   1.401 @@ -958,7 +958,7 @@
   1.402    shows "P n"
   1.403    by (rule less_induct) (auto intro: step simp:le_simps)
   1.404  
   1.405 -text{*An induction rule for estabilishing binary relations*}
   1.406 +text\<open>An induction rule for estabilishing binary relations\<close>
   1.407  lemma less_Suc_induct:
   1.408    assumes less:  "i < j"
   1.409       and  step:  "!!i. P i (Suc i)"
   1.410 @@ -980,16 +980,16 @@
   1.411    thus "P i j" by (simp add: j)
   1.412  qed
   1.413  
   1.414 -text {* The method of infinite descent, frequently used in number theory.
   1.415 +text \<open>The method of infinite descent, frequently used in number theory.
   1.416  Provided by Roelof Oosterhuis.
   1.417  $P(n)$ is true for all $n\in\mathbb{N}$ if
   1.418  \begin{itemize}
   1.419    \item case ``0'': given $n=0$ prove $P(n)$,
   1.420    \item case ``smaller'': given $n>0$ and $\neg P(n)$ prove there exists
   1.421          a smaller integer $m$ such that $\neg P(m)$.
   1.422 -\end{itemize} *}
   1.423 -
   1.424 -text{* A compact version without explicit base case: *}
   1.425 +\end{itemize}\<close>
   1.426 +
   1.427 +text\<open>A compact version without explicit base case:\<close>
   1.428  lemma infinite_descent:
   1.429    "\<lbrakk> !!n::nat. \<not> P n \<Longrightarrow>  \<exists>m<n. \<not>  P m \<rbrakk> \<Longrightarrow>  P n"
   1.430  by (induct n rule: less_induct) auto
   1.431 @@ -998,14 +998,14 @@
   1.432    "\<lbrakk> P 0; !!n. n>0 \<Longrightarrow> \<not> P n \<Longrightarrow> (\<exists>m::nat. m < n \<and> \<not>P m) \<rbrakk> \<Longrightarrow> P n"
   1.433  by (rule infinite_descent) (case_tac "n>0", auto)
   1.434  
   1.435 -text {*
   1.436 +text \<open>
   1.437  Infinite descent using a mapping to $\mathbb{N}$:
   1.438  $P(x)$ is true for all $x\in D$ if there exists a $V: D \to \mathbb{N}$ and
   1.439  \begin{itemize}
   1.440  \item case ``0'': given $V(x)=0$ prove $P(x)$,
   1.441  \item case ``smaller'': given $V(x)>0$ and $\neg P(x)$ prove there exists a $y \in D$ such that $V(y)<V(x)$ and $~\neg P(y)$.
   1.442  \end{itemize}
   1.443 -NB: the proof also shows how to use the previous lemma. *}
   1.444 +NB: the proof also shows how to use the previous lemma.\<close>
   1.445  
   1.446  corollary infinite_descent0_measure [case_names 0 smaller]:
   1.447    assumes A0: "!!x. V x = (0::nat) \<Longrightarrow> P x"
   1.448 @@ -1027,7 +1027,7 @@
   1.449    ultimately show "P x" by auto
   1.450  qed
   1.451  
   1.452 -text{* Again, without explicit base case: *}
   1.453 +text\<open>Again, without explicit base case:\<close>
   1.454  lemma infinite_descent_measure:
   1.455  assumes "!!x. \<not> P x \<Longrightarrow> \<exists>y. (V::'a\<Rightarrow>nat) y < V x \<and> \<not> P y" shows "P x"
   1.456  proof -
   1.457 @@ -1040,18 +1040,18 @@
   1.458    ultimately show "P x" by auto
   1.459  qed
   1.460  
   1.461 -text {* A [clumsy] way of lifting @{text "<"}
   1.462 -  monotonicity to @{text "\<le>"} monotonicity *}
   1.463 +text \<open>A [clumsy] way of lifting @{text "<"}
   1.464 +  monotonicity to @{text "\<le>"} monotonicity\<close>
   1.465  lemma less_mono_imp_le_mono:
   1.466    "\<lbrakk> !!i j::nat. i < j \<Longrightarrow> f i < f j; i \<le> j \<rbrakk> \<Longrightarrow> f i \<le> ((f j)::nat)"
   1.467  by (simp add: order_le_less) (blast)
   1.468  
   1.469  
   1.470 -text {* non-strict, in 1st argument *}
   1.471 +text \<open>non-strict, in 1st argument\<close>
   1.472  lemma add_le_mono1: "i \<le> j ==> i + k \<le> j + (k::nat)"
   1.473  by (rule add_right_mono)
   1.474  
   1.475 -text {* non-strict, in both arguments *}
   1.476 +text \<open>non-strict, in both arguments\<close>
   1.477  lemma add_le_mono: "[| i \<le> j;  k \<le> l |] ==> i + k \<le> j + (l::nat)"
   1.478  by (rule add_mono)
   1.479  
   1.480 @@ -1109,13 +1109,13 @@
   1.481  lemma add_leE: "(m::nat) + k \<le> n ==> (m \<le> n ==> k \<le> n ==> R) ==> R"
   1.482  by (blast dest: add_leD1 add_leD2)
   1.483  
   1.484 -text {* needs @{text "!!k"} for @{text ac_simps} to work *}
   1.485 +text \<open>needs @{text "!!k"} for @{text ac_simps} to work\<close>
   1.486  lemma less_add_eq_less: "!!k::nat. k < l ==> m + l = k + n ==> m < n"
   1.487  by (force simp del: add_Suc_right
   1.488      simp add: less_iff_Suc_add add_Suc_right [symmetric] ac_simps)
   1.489  
   1.490  
   1.491 -subsubsection {* More results about difference *}
   1.492 +subsubsection \<open>More results about difference\<close>
   1.493  
   1.494  lemma Suc_diff_le: "n \<le> m ==> Suc m - n = Suc (m - n)"
   1.495  by (induct m n rule: diff_induct) simp_all
   1.496 @@ -1169,7 +1169,7 @@
   1.497      by (simp add: order_less_imp_le)
   1.498  qed
   1.499  
   1.500 -text {* a nice rewrite for bounded subtraction *}
   1.501 +text \<open>a nice rewrite for bounded subtraction\<close>
   1.502  lemma nat_minus_add_max:
   1.503    fixes n m :: nat
   1.504    shows "n - m + m = max n m"
   1.505 @@ -1177,14 +1177,14 @@
   1.506  
   1.507  lemma nat_diff_split:
   1.508    "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
   1.509 -    -- {* elimination of @{text -} on @{text nat} *}
   1.510 +    -- \<open>elimination of @{text -} on @{text nat}\<close>
   1.511  by (cases "a < b")
   1.512    (auto simp add: diff_is_0_eq [THEN iffD2] diff_add_inverse
   1.513      not_less le_less dest!: add_eq_self_zero add_eq_self_zero[OF sym])
   1.514  
   1.515  lemma nat_diff_split_asm:
   1.516    "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
   1.517 -    -- {* elimination of @{text -} on @{text nat} in assumptions *}
   1.518 +    -- \<open>elimination of @{text -} on @{text nat} in assumptions\<close>
   1.519  by (auto split: nat_diff_split)
   1.520  
   1.521  lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
   1.522 @@ -1206,7 +1206,7 @@
   1.523    by (fact Let_def)
   1.524  
   1.525  
   1.526 -subsubsection {* Monotonicity of multiplication *}
   1.527 +subsubsection \<open>Monotonicity of multiplication\<close>
   1.528  
   1.529  lemma mult_le_mono1: "i \<le> (j::nat) ==> i * k \<le> j * k"
   1.530  by (simp add: mult_right_mono)
   1.531 @@ -1214,15 +1214,15 @@
   1.532  lemma mult_le_mono2: "i \<le> (j::nat) ==> k * i \<le> k * j"
   1.533  by (simp add: mult_left_mono)
   1.534  
   1.535 -text {* @{text "\<le>"} monotonicity, BOTH arguments *}
   1.536 +text \<open>@{text "\<le>"} monotonicity, BOTH arguments\<close>
   1.537  lemma mult_le_mono: "i \<le> (j::nat) ==> k \<le> l ==> i * k \<le> j * l"
   1.538  by (simp add: mult_mono)
   1.539  
   1.540  lemma mult_less_mono1: "(i::nat) < j ==> 0 < k ==> i * k < j * k"
   1.541  by (simp add: mult_strict_right_mono)
   1.542  
   1.543 -text{*Differs from the standard @{text zero_less_mult_iff} in that
   1.544 -      there are no negative numbers.*}
   1.545 +text\<open>Differs from the standard @{text zero_less_mult_iff} in that
   1.546 +      there are no negative numbers.\<close>
   1.547  lemma nat_0_less_mult_iff [simp]: "(0 < (m::nat) * n) = (0 < m & 0 < n)"
   1.548    apply (induct m)
   1.549     apply simp
   1.550 @@ -1265,7 +1265,7 @@
   1.551  lemma le_cube: "(m::nat) \<le> m * (m * m)"
   1.552    by (cases m) (auto intro: le_add1)
   1.553  
   1.554 -text {* Lemma for @{text gcd} *}
   1.555 +text \<open>Lemma for @{text gcd}\<close>
   1.556  lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = 1 | m = 0"
   1.557    apply (drule sym)
   1.558    apply (rule disjCI)
   1.559 @@ -1284,7 +1284,7 @@
   1.560    with assms show "n * m \<le> n * q" by simp
   1.561  qed
   1.562  
   1.563 -text {* the lattice order on @{typ nat} *}
   1.564 +text \<open>the lattice order on @{typ nat}\<close>
   1.565  
   1.566  instantiation nat :: distrib_lattice
   1.567  begin
   1.568 @@ -1302,12 +1302,12 @@
   1.569  end
   1.570  
   1.571  
   1.572 -subsection {* Natural operation of natural numbers on functions *}
   1.573 -
   1.574 -text {*
   1.575 +subsection \<open>Natural operation of natural numbers on functions\<close>
   1.576 +
   1.577 +text \<open>
   1.578    We use the same logical constant for the power operations on
   1.579    functions and relations, in order to share the same syntax.
   1.580 -*}
   1.581 +\<close>
   1.582  
   1.583  consts compow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
   1.584  
   1.585 @@ -1320,7 +1320,7 @@
   1.586  notation (HTML output)
   1.587    compower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
   1.588  
   1.589 -text {* @{text "f ^^ n = f o ... o f"}, the n-fold composition of @{text f} *}
   1.590 +text \<open>@{text "f ^^ n = f o ... o f"}, the n-fold composition of @{text f}\<close>
   1.591  
   1.592  overloading
   1.593    funpow == "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
   1.594 @@ -1345,7 +1345,7 @@
   1.595  
   1.596  lemmas funpow_simps_right = funpow.simps(1) funpow_Suc_right
   1.597  
   1.598 -text {* for code generation *}
   1.599 +text \<open>for code generation\<close>
   1.600  
   1.601  definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
   1.602    funpow_code_def [code_abbrev]: "funpow = compow"
   1.603 @@ -1392,7 +1392,7 @@
   1.604    by (induct n arbitrary: A B)
   1.605       (auto simp del: funpow.simps(2) simp add: funpow_Suc_right mono_def)
   1.606  
   1.607 -subsection {* Kleene iteration *}
   1.608 +subsection \<open>Kleene iteration\<close>
   1.609  
   1.610  lemma Kleene_iter_lpfp:
   1.611  assumes "mono f" and "f p \<le> p" shows "(f^^k) (bot::'a::order_bot) \<le> p"
   1.612 @@ -1453,7 +1453,7 @@
   1.613      by (intro gfp_upperbound) (simp del: funpow.simps)
   1.614  qed
   1.615  
   1.616 -subsection {* Embedding of the naturals into any @{text semiring_1}: @{term of_nat} *}
   1.617 +subsection \<open>Embedding of the naturals into any @{text semiring_1}: @{term of_nat}\<close>
   1.618  
   1.619  context semiring_1
   1.620  begin
   1.621 @@ -1477,7 +1477,7 @@
   1.622  
   1.623  primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
   1.624    "of_nat_aux inc 0 i = i"
   1.625 -| "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" -- {* tail recursive *}
   1.626 +| "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" -- \<open>tail recursive\<close>
   1.627  
   1.628  lemma of_nat_code:
   1.629    "of_nat n = of_nat_aux (\<lambda>i. i + 1) n 0"
   1.630 @@ -1496,8 +1496,8 @@
   1.631  
   1.632  declare of_nat_code [code]
   1.633  
   1.634 -text{*Class for unital semirings with characteristic zero.
   1.635 - Includes non-ordered rings like the complex numbers.*}
   1.636 +text\<open>Class for unital semirings with characteristic zero.
   1.637 + Includes non-ordered rings like the complex numbers.\<close>
   1.638  
   1.639  class semiring_char_0 = semiring_1 +
   1.640    assumes inj_of_nat: "inj of_nat"
   1.641 @@ -1506,7 +1506,7 @@
   1.642  lemma of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n"
   1.643    by (auto intro: inj_of_nat injD)
   1.644  
   1.645 -text{*Special cases where either operand is zero*}
   1.646 +text\<open>Special cases where either operand is zero\<close>
   1.647  
   1.648  lemma of_nat_0_eq_iff [simp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
   1.649    by (fact of_nat_eq_iff [of 0 n, unfolded of_nat_0])
   1.650 @@ -1545,12 +1545,12 @@
   1.651  lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n"
   1.652    by simp
   1.653  
   1.654 -text{*Every @{text linordered_semidom} has characteristic zero.*}
   1.655 +text\<open>Every @{text linordered_semidom} has characteristic zero.\<close>
   1.656  
   1.657  subclass semiring_char_0 proof
   1.658  qed (auto intro!: injI simp add: eq_iff)
   1.659  
   1.660 -text{*Special cases where either operand is zero*}
   1.661 +text\<open>Special cases where either operand is zero\<close>
   1.662  
   1.663  lemma of_nat_le_0_iff [simp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
   1.664    by (rule of_nat_le_iff [of _ 0, simplified])
   1.665 @@ -1583,7 +1583,7 @@
   1.666    by (auto simp add: fun_eq_iff)
   1.667  
   1.668  
   1.669 -subsection {* The set of natural numbers *}
   1.670 +subsection \<open>The set of natural numbers\<close>
   1.671  
   1.672  context semiring_1
   1.673  begin
   1.674 @@ -1626,7 +1626,7 @@
   1.675    obtains (of_nat) n where "x = of_nat n"
   1.676    unfolding Nats_def
   1.677  proof -
   1.678 -  from `x \<in> \<nat>` have "x \<in> range of_nat" unfolding Nats_def .
   1.679 +  from \<open>x \<in> \<nat>\<close> have "x \<in> range of_nat" unfolding Nats_def .
   1.680    then obtain n where "x = of_nat n" ..
   1.681    then show thesis ..
   1.682  qed
   1.683 @@ -1638,7 +1638,7 @@
   1.684  end
   1.685  
   1.686  
   1.687 -subsection {* Further arithmetic facts concerning the natural numbers *}
   1.688 +subsection \<open>Further arithmetic facts concerning the natural numbers\<close>
   1.689  
   1.690  lemma subst_equals:
   1.691    assumes 1: "t = s" and 2: "u = t"
   1.692 @@ -1649,26 +1649,26 @@
   1.693  
   1.694  simproc_setup nateq_cancel_sums
   1.695    ("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") =
   1.696 -  {* fn phi => try o Nat_Arith.cancel_eq_conv *}
   1.697 +  \<open>fn phi => try o Nat_Arith.cancel_eq_conv\<close>
   1.698  
   1.699  simproc_setup natless_cancel_sums
   1.700    ("(l::nat) + m < n" | "(l::nat) < m + n" | "Suc m < n" | "m < Suc n") =
   1.701 -  {* fn phi => try o Nat_Arith.cancel_less_conv *}
   1.702 +  \<open>fn phi => try o Nat_Arith.cancel_less_conv\<close>
   1.703  
   1.704  simproc_setup natle_cancel_sums
   1.705    ("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" | "Suc m \<le> n" | "m \<le> Suc n") =
   1.706 -  {* fn phi => try o Nat_Arith.cancel_le_conv *}
   1.707 +  \<open>fn phi => try o Nat_Arith.cancel_le_conv\<close>
   1.708  
   1.709  simproc_setup natdiff_cancel_sums
   1.710    ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") =
   1.711 -  {* fn phi => try o Nat_Arith.cancel_diff_conv *}
   1.712 +  \<open>fn phi => try o Nat_Arith.cancel_diff_conv\<close>
   1.713  
   1.714  ML_file "Tools/lin_arith.ML"
   1.715 -setup {* Lin_Arith.global_setup *}
   1.716 -declaration {* K Lin_Arith.setup *}
   1.717 +setup \<open>Lin_Arith.global_setup\<close>
   1.718 +declaration \<open>K Lin_Arith.setup\<close>
   1.719  
   1.720  simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) <= n" | "(m::nat) = n") =
   1.721 -  {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (Thm.term_of ct) *}
   1.722 +  \<open>fn _ => fn ss => fn ct => Lin_Arith.simproc ss (Thm.term_of ct)\<close>
   1.723  (* Because of this simproc, the arithmetic solver is really only
   1.724  useful to detect inconsistencies among the premises for subgoals which are
   1.725  *not* themselves (in)equalities, because the latter activate
   1.726 @@ -1688,7 +1688,7 @@
   1.727    case True
   1.728    then show ?thesis
   1.729      by (induct n n' rule: less_Suc_induct [consumes 1]) (auto intro: mono)
   1.730 -qed (insert `n \<le> n'`, auto) -- {* trivial for @{prop "n = n'"} *}
   1.731 +qed (insert \<open>n \<le> n'\<close>, auto) -- \<open>trivial for @{prop "n = n'"}\<close>
   1.732  
   1.733  lemma lift_Suc_antimono_le:
   1.734    assumes mono: "\<And>n. f n \<ge> f (Suc n)" and "n \<le> n'"
   1.735 @@ -1697,12 +1697,12 @@
   1.736    case True
   1.737    then show ?thesis
   1.738      by (induct n n' rule: less_Suc_induct [consumes 1]) (auto intro: mono)
   1.739 -qed (insert `n \<le> n'`, auto) -- {* trivial for @{prop "n = n'"} *}
   1.740 +qed (insert \<open>n \<le> n'\<close>, auto) -- \<open>trivial for @{prop "n = n'"}\<close>
   1.741  
   1.742  lemma lift_Suc_mono_less:
   1.743    assumes mono: "\<And>n. f n < f (Suc n)" and "n < n'"
   1.744    shows "f n < f n'"
   1.745 -using `n < n'`
   1.746 +using \<open>n < n'\<close>
   1.747  by (induct n n' rule: less_Suc_induct [consumes 1]) (auto intro: mono)
   1.748  
   1.749  lemma lift_Suc_mono_less_iff:
   1.750 @@ -1735,7 +1735,7 @@
   1.751  qed
   1.752  
   1.753  
   1.754 -text{*Subtraction laws, mostly by Clemens Ballarin*}
   1.755 +text\<open>Subtraction laws, mostly by Clemens Ballarin\<close>
   1.756  
   1.757  lemma diff_less_mono: "[| a < (b::nat); c \<le> a |] ==> a-c < b-c"
   1.758  by arith
   1.759 @@ -1753,20 +1753,20 @@
   1.760  by arith
   1.761  
   1.762  lemma le_diff_conv2: "k \<le> j ==> (i \<le> j-k) = (i+k \<le> (j::nat))"
   1.763 -  by (fact le_diff_conv2) -- {* FIXME delete *}
   1.764 +  by (fact le_diff_conv2) -- \<open>FIXME delete\<close>
   1.765  
   1.766  lemma diff_diff_cancel [simp]: "i \<le> (n::nat) ==> n - (n - i) = i"
   1.767  by arith
   1.768  
   1.769  lemma le_add_diff: "k \<le> (n::nat) ==> m \<le> n + m - k"
   1.770 -  by (fact le_add_diff) -- {* FIXME delete *}
   1.771 +  by (fact le_add_diff) -- \<open>FIXME delete\<close>
   1.772  
   1.773  (*Replaces the previous diff_less and le_diff_less, which had the stronger
   1.774    second premise n\<le>m*)
   1.775  lemma diff_less[simp]: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m"
   1.776  by arith
   1.777  
   1.778 -text {* Simplification of relational expressions involving subtraction *}
   1.779 +text \<open>Simplification of relational expressions involving subtraction\<close>
   1.780  
   1.781  lemma diff_diff_eq: "[| k \<le> m;  k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"
   1.782  by (simp split add: nat_diff_split)
   1.783 @@ -1782,7 +1782,7 @@
   1.784  lemma le_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k \<le> n-k) = (m\<le>n)"
   1.785  by (auto split add: nat_diff_split)
   1.786  
   1.787 -text{*(Anti)Monotonicity of subtraction -- by Stephan Merz*}
   1.788 +text\<open>(Anti)Monotonicity of subtraction -- by Stephan Merz\<close>
   1.789  
   1.790  (* Monotonicity of subtraction in first argument *)
   1.791  lemma diff_le_mono: "m \<le> (n::nat) ==> (m-l) \<le> (n-l)"
   1.792 @@ -1810,7 +1810,7 @@
   1.793    with a k_le_n show "x = y" by auto
   1.794  qed
   1.795  
   1.796 -text{*Rewriting to pull differences out*}
   1.797 +text\<open>Rewriting to pull differences out\<close>
   1.798  
   1.799  lemma diff_diff_right [simp]: "k\<le>j --> i - (j - k) = i + (k::nat) - j"
   1.800  by arith
   1.801 @@ -1832,10 +1832,10 @@
   1.802  lemmas add_diff_assoc2 = diff_add_assoc2[symmetric]
   1.803  declare diff_diff_left [simp]  add_diff_assoc [simp] add_diff_assoc2[simp]
   1.804  
   1.805 -text{*At present we prove no analogue of @{text not_less_Least} or @{text
   1.806 -Least_Suc}, since there appears to be no need.*}
   1.807 -
   1.808 -text{*Lemmas for ex/Factorization*}
   1.809 +text\<open>At present we prove no analogue of @{text not_less_Least} or @{text
   1.810 +Least_Suc}, since there appears to be no need.\<close>
   1.811 +
   1.812 +text\<open>Lemmas for ex/Factorization\<close>
   1.813  
   1.814  lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
   1.815  by (cases m) auto
   1.816 @@ -1846,7 +1846,7 @@
   1.817  lemma n_less_n_mult_m: "[| Suc 0 < n; Suc 0 < m |] ==> n<n*m"
   1.818  by (cases m) auto
   1.819  
   1.820 -text {* Specialized induction principles that work "backwards": *}
   1.821 +text \<open>Specialized induction principles that work "backwards":\<close>
   1.822  
   1.823  lemma inc_induct[consumes 1, case_names base step]:
   1.824    assumes less: "i \<le> j"
   1.825 @@ -1873,7 +1873,7 @@
   1.826    using less
   1.827  proof (induct d=="j - i - 1" arbitrary: i)
   1.828    case (0 i)
   1.829 -  with `i < j` have "j = Suc i" by simp
   1.830 +  with \<open>i < j\<close> have "j = Suc i" by simp
   1.831    with base show ?case by simp
   1.832  next
   1.833    case (Suc d i)
   1.834 @@ -1888,7 +1888,7 @@
   1.835  lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0"
   1.836    using inc_induct[of 0 k P] by blast
   1.837  
   1.838 -text {* Further induction rule similar to @{thm inc_induct} *}
   1.839 +text \<open>Further induction rule similar to @{thm inc_induct}\<close>
   1.840  
   1.841  lemma dec_induct[consumes 1, case_names base step]:
   1.842    "i \<le> j \<Longrightarrow> P i \<Longrightarrow> (\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P j"
   1.843 @@ -1920,7 +1920,7 @@
   1.844    shows "mono Q \<Longrightarrow> antimono (\<lambda>i. (Q ^^ i) \<top>)"
   1.845    by (auto intro!: funpow_increasing simp: antimono_def)
   1.846  
   1.847 -subsection {* The divides relation on @{typ nat} *}
   1.848 +subsection \<open>The divides relation on @{typ nat}\<close>
   1.849  
   1.850  lemma dvd_1_left [iff]: "Suc 0 dvd k"
   1.851  unfolding dvd_def by simp
   1.852 @@ -1935,7 +1935,7 @@
   1.853    unfolding dvd_def
   1.854    by (force dest: mult_eq_self_implies_10 simp add: mult.assoc)
   1.855  
   1.856 -text {* @{term "op dvd"} is a partial order *}
   1.857 +text \<open>@{term "op dvd"} is a partial order\<close>
   1.858  
   1.859  interpretation dvd: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"
   1.860    proof qed (auto intro: dvd_refl dvd_trans dvd_antisym)
   1.861 @@ -2006,7 +2006,7 @@
   1.862  qed
   1.863  
   1.864  
   1.865 -subsection {* Aliases *}
   1.866 +subsection \<open>Aliases\<close>
   1.867  
   1.868  lemma nat_mult_1: "(1::nat) * n = n"
   1.869    by (fact mult_1_left)
   1.870 @@ -2015,10 +2015,10 @@
   1.871    by (fact mult_1_right)
   1.872  
   1.873  
   1.874 -subsection {* Size of a datatype value *}
   1.875 +subsection \<open>Size of a datatype value\<close>
   1.876  
   1.877  class size =
   1.878 -  fixes size :: "'a \<Rightarrow> nat" -- {* see further theory @{text Wellfounded} *}
   1.879 +  fixes size :: "'a \<Rightarrow> nat" -- \<open>see further theory @{text Wellfounded}\<close>
   1.880  
   1.881  instantiation nat :: size
   1.882  begin
   1.883 @@ -2031,7 +2031,7 @@
   1.884  end
   1.885  
   1.886  
   1.887 -subsection {* Code module namespace *}
   1.888 +subsection \<open>Code module namespace\<close>
   1.889  
   1.890  code_identifier
   1.891    code_module Nat \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith