isabelle update_cartouches;
authorwenzelm
Sat Oct 10 16:26:23 2015 +0200 (2015-10-10)
changeset 61382efac889fccbc
parent 61381 ddca85598c65
child 61383 6762c8445138
isabelle update_cartouches;
src/HOL/Algebra/AbelCoset.thy
src/HOL/Algebra/Bij.thy
src/HOL/Algebra/Congruence.thy
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/Divisibility.thy
src/HOL/Algebra/Exponent.thy
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Ideal.thy
src/HOL/Algebra/IntRing.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/Module.thy
src/HOL/Algebra/QuotRing.thy
src/HOL/Algebra/Ring.thy
src/HOL/Algebra/RingHom.thy
src/HOL/Algebra/Sylow.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Old_Number_Theory/BijectionRel.thy
src/HOL/Old_Number_Theory/Chinese.thy
src/HOL/Old_Number_Theory/Euler.thy
src/HOL/Old_Number_Theory/EulerFermat.thy
src/HOL/Old_Number_Theory/EvenOdd.thy
src/HOL/Old_Number_Theory/Factorization.thy
src/HOL/Old_Number_Theory/Fib.thy
src/HOL/Old_Number_Theory/Finite2.thy
src/HOL/Old_Number_Theory/Gauss.thy
src/HOL/Old_Number_Theory/Int2.thy
src/HOL/Old_Number_Theory/IntFact.thy
src/HOL/Old_Number_Theory/IntPrimes.thy
src/HOL/Old_Number_Theory/Legacy_GCD.thy
src/HOL/Old_Number_Theory/Pocklington.thy
src/HOL/Old_Number_Theory/Primes.thy
src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
src/HOL/Old_Number_Theory/Residues.thy
src/HOL/Old_Number_Theory/WilsonBij.thy
src/HOL/Old_Number_Theory/WilsonRuss.thy
     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Sat Oct 10 16:21:34 2015 +0200
     1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Sat Oct 10 16:26:23 2015 +0200
     1.3 @@ -6,12 +6,12 @@
     1.4  imports Coset Ring
     1.5  begin
     1.6  
     1.7 -subsection {* More Lifting from Groups to Abelian Groups *}
     1.8 +subsection \<open>More Lifting from Groups to Abelian Groups\<close>
     1.9  
    1.10 -subsubsection {* Definitions *}
    1.11 +subsubsection \<open>Definitions\<close>
    1.12  
    1.13 -text {* Hiding @{text "<+>"} from @{theory Sum_Type} until I come
    1.14 -  up with better syntax here *}
    1.15 +text \<open>Hiding @{text "<+>"} from @{theory Sum_Type} until I come
    1.16 +  up with better syntax here\<close>
    1.17  
    1.18  no_notation Sum_Type.Plus (infixr "<+>" 65)
    1.19  
    1.20 @@ -41,12 +41,12 @@
    1.21  
    1.22  definition
    1.23    A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "A'_Mod" 65)
    1.24 -    --{*Actually defined for groups rather than monoids*}
    1.25 +    --\<open>Actually defined for groups rather than monoids\<close>
    1.26    where "A_FactGroup G H = FactGroup \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
    1.27  
    1.28  definition
    1.29    a_kernel :: "('a, 'm) ring_scheme \<Rightarrow> ('b, 'n) ring_scheme \<Rightarrow>  ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
    1.30 -    --{*the kernel of a homomorphism (additive)*}
    1.31 +    --\<open>the kernel of a homomorphism (additive)\<close>
    1.32    where "a_kernel G H h =
    1.33      kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
    1.34        \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
    1.35 @@ -103,7 +103,7 @@
    1.36  by (fold a_inv_def)
    1.37  
    1.38  
    1.39 -subsubsection {* Cosets *}
    1.40 +subsubsection \<open>Cosets\<close>
    1.41  
    1.42  lemma (in abelian_group) a_coset_add_assoc:
    1.43       "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
    1.44 @@ -163,7 +163,7 @@
    1.45  by (rule group.rcosetsI [OF a_group,
    1.46      folded a_r_coset_def A_RCOSETS_def, simplified monoid_record_simps])
    1.47  
    1.48 -text{*Really needed?*}
    1.49 +text\<open>Really needed?\<close>
    1.50  lemma (in abelian_group) a_transpose_inv:
    1.51       "[| x \<oplus> y = z;  x \<in> carrier G;  y \<in> carrier G;  z \<in> carrier G |]
    1.52        ==> (\<ominus> x) \<oplus> z = y"
    1.53 @@ -179,7 +179,7 @@
    1.54  *)
    1.55  
    1.56  
    1.57 -subsubsection {* Subgroups *}
    1.58 +subsubsection \<open>Subgroups\<close>
    1.59  
    1.60  locale additive_subgroup =
    1.61    fixes H and G (structure)
    1.62 @@ -216,9 +216,9 @@
    1.63      folded a_inv_def, simplified monoid_record_simps])
    1.64  
    1.65  
    1.66 -subsubsection {* Additive subgroups are normal *}
    1.67 +subsubsection \<open>Additive subgroups are normal\<close>
    1.68  
    1.69 -text {* Every subgroup of an @{text "abelian_group"} is normal *}
    1.70 +text \<open>Every subgroup of an @{text "abelian_group"} is normal\<close>
    1.71  
    1.72  locale abelian_subgroup = additive_subgroup + abelian_group G +
    1.73    assumes a_normal: "normal H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.74 @@ -287,7 +287,7 @@
    1.75  by (rule normal.inv_op_closed2 [OF a_normal,
    1.76      folded a_inv_def, simplified monoid_record_simps])
    1.77  
    1.78 -text{*Alternative characterization of normal subgroups*}
    1.79 +text\<open>Alternative characterization of normal subgroups\<close>
    1.80  lemma (in abelian_group) a_normal_inv_iff:
    1.81       "(N \<lhd> \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>) = 
    1.82        (subgroup N \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> & (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<oplus> h \<oplus> (\<ominus> x) \<in> N))"
    1.83 @@ -378,12 +378,12 @@
    1.84  
    1.85  lemma (in abelian_subgroup) rcosets_add_eq:
    1.86    "M \<in> a_rcosets H \<Longrightarrow> H <+> M = M"
    1.87 -  -- {* generalizes @{text subgroup_mult_id} *}
    1.88 +  -- \<open>generalizes @{text subgroup_mult_id}\<close>
    1.89  by (rule normal.rcosets_mult_eq [OF a_normal,
    1.90      folded set_add_def A_RCOSETS_def, simplified monoid_record_simps])
    1.91  
    1.92  
    1.93 -subsubsection {* Congruence Relation *}
    1.94 +subsubsection \<open>Congruence Relation\<close>
    1.95  
    1.96  lemma (in abelian_subgroup) a_equiv_rcong:
    1.97     shows "equiv (carrier G) (racong H)"
    1.98 @@ -444,7 +444,7 @@
    1.99      (fast intro!: additive_subgroup.a_subgroup)+
   1.100  
   1.101  
   1.102 -subsubsection {* Factorization *}
   1.103 +subsubsection \<open>Factorization\<close>
   1.104  
   1.105  lemmas A_FactGroup_defs = A_FactGroup_def FactGroup_def
   1.106  
   1.107 @@ -486,8 +486,8 @@
   1.108  by (rule normal.factorgroup_is_group [OF a_normal,
   1.109      folded A_FactGroup_def, simplified monoid_record_simps])
   1.110  
   1.111 -text {* Since the Factorization is based on an \emph{abelian} subgroup, is results in 
   1.112 -        a commutative group *}
   1.113 +text \<open>Since the Factorization is based on an \emph{abelian} subgroup, is results in 
   1.114 +        a commutative group\<close>
   1.115  theorem (in abelian_subgroup) a_factorgroup_is_comm_group:
   1.116    "comm_group (G A_Mod H)"
   1.117  apply (intro comm_group.intro comm_monoid.intro) prefer 3
   1.118 @@ -506,21 +506,21 @@
   1.119  by (rule normal.inv_FactGroup [OF a_normal,
   1.120      folded A_FactGroup_def A_SET_INV_def, simplified monoid_record_simps])
   1.121  
   1.122 -text{*The coset map is a homomorphism from @{term G} to the quotient group
   1.123 -  @{term "G Mod H"}*}
   1.124 +text\<open>The coset map is a homomorphism from @{term G} to the quotient group
   1.125 +  @{term "G Mod H"}\<close>
   1.126  lemma (in abelian_subgroup) a_r_coset_hom_A_Mod:
   1.127    "(\<lambda>a. H +> a) \<in> hom \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> (G A_Mod H)"
   1.128  by (rule normal.r_coset_hom_Mod [OF a_normal,
   1.129      folded A_FactGroup_def a_r_coset_def, simplified monoid_record_simps])
   1.130  
   1.131 -text {* The isomorphism theorems have been omitted from lifting, at
   1.132 -  least for now *}
   1.133 +text \<open>The isomorphism theorems have been omitted from lifting, at
   1.134 +  least for now\<close>
   1.135  
   1.136  
   1.137 -subsubsection{*The First Isomorphism Theorem*}
   1.138 +subsubsection\<open>The First Isomorphism Theorem\<close>
   1.139  
   1.140 -text{*The quotient by the kernel of a homomorphism is isomorphic to the 
   1.141 -  range of that homomorphism.*}
   1.142 +text\<open>The quotient by the kernel of a homomorphism is isomorphic to the 
   1.143 +  range of that homomorphism.\<close>
   1.144  
   1.145  lemmas a_kernel_defs =
   1.146    a_kernel_def kernel_def
   1.147 @@ -530,7 +530,7 @@
   1.148  by (rule a_kernel_def[unfolded kernel_def, simplified ring_record_simps])
   1.149  
   1.150  
   1.151 -subsubsection {* Homomorphisms *}
   1.152 +subsubsection \<open>Homomorphisms\<close>
   1.153  
   1.154  lemma abelian_group_homI:
   1.155    assumes "abelian_group G"
   1.156 @@ -591,7 +591,7 @@
   1.157         folded a_kernel_def, simplified ring_record_simps])
   1.158  done
   1.159  
   1.160 -text{*The kernel of a homomorphism is an abelian subgroup*}
   1.161 +text\<open>The kernel of a homomorphism is an abelian subgroup\<close>
   1.162  lemma (in abelian_group_hom) abelian_subgroup_a_kernel:
   1.163    "abelian_subgroup (a_kernel G H h) G"
   1.164  apply (rule abelian_subgroupI)
   1.165 @@ -623,16 +623,16 @@
   1.166  by (rule group_hom.FactGroup_inj_on[OF a_group_hom,
   1.167      folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
   1.168  
   1.169 -text{*If the homomorphism @{term h} is onto @{term H}, then so is the
   1.170 -homomorphism from the quotient group*}
   1.171 +text\<open>If the homomorphism @{term h} is onto @{term H}, then so is the
   1.172 +homomorphism from the quotient group\<close>
   1.173  lemma (in abelian_group_hom) A_FactGroup_onto:
   1.174    assumes h: "h ` carrier G = carrier H"
   1.175    shows "(\<lambda>X. the_elem (h ` X)) ` carrier (G A_Mod a_kernel G H h) = carrier H"
   1.176  by (rule group_hom.FactGroup_onto[OF a_group_hom,
   1.177      folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule h)
   1.178  
   1.179 -text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
   1.180 - quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
   1.181 +text\<open>If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
   1.182 + quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.\<close>
   1.183  theorem (in abelian_group_hom) A_FactGroup_iso:
   1.184    "h ` carrier G = carrier H
   1.185     \<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> (G A_Mod (a_kernel G H h)) \<cong>
   1.186 @@ -641,9 +641,9 @@
   1.187      folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
   1.188  
   1.189  
   1.190 -subsubsection {* Cosets *}
   1.191 +subsubsection \<open>Cosets\<close>
   1.192  
   1.193 -text {* Not eveything from \texttt{CosetExt.thy} is lifted here. *}
   1.194 +text \<open>Not eveything from \texttt{CosetExt.thy} is lifted here.\<close>
   1.195  
   1.196  lemma (in additive_subgroup) a_Hcarr [simp]:
   1.197    assumes hH: "h \<in> H"
   1.198 @@ -725,7 +725,7 @@
   1.199      folded A_RCOSETS_def, simplified monoid_record_simps])
   1.200  
   1.201  
   1.202 -subsubsection {* Addition of Subgroups *}
   1.203 +subsubsection \<open>Addition of Subgroups\<close>
   1.204  
   1.205  lemma (in abelian_monoid) set_add_closed:
   1.206    assumes Acarr: "A \<subseteq> carrier G"
     2.1 --- a/src/HOL/Algebra/Bij.thy	Sat Oct 10 16:21:34 2015 +0200
     2.2 +++ b/src/HOL/Algebra/Bij.thy	Sat Oct 10 16:26:23 2015 +0200
     2.3 @@ -6,11 +6,11 @@
     2.4  imports Group
     2.5  begin
     2.6  
     2.7 -section {* Bijections of a Set, Permutation and Automorphism Groups *}
     2.8 +section \<open>Bijections of a Set, Permutation and Automorphism Groups\<close>
     2.9  
    2.10  definition
    2.11    Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set"
    2.12 -    --{*Only extensional functions, since otherwise we get too many.*}
    2.13 +    --\<open>Only extensional functions, since otherwise we get too many.\<close>
    2.14     where "Bij S = extensional S \<inter> {f. bij_betw f S S}"
    2.15  
    2.16  definition
    2.17 @@ -30,7 +30,7 @@
    2.18    by (auto simp add: Bij_def bij_betw_imp_funcset)
    2.19  
    2.20  
    2.21 -subsection {*Bijections Form a Group *}
    2.22 +subsection \<open>Bijections Form a Group\<close>
    2.23  
    2.24  lemma restrict_inv_into_Bij: "f \<in> Bij S \<Longrightarrow> (\<lambda>x \<in> S. (inv_into S f) x) \<in> Bij S"
    2.25    by (simp add: Bij_def bij_betw_inv_into)
    2.26 @@ -57,7 +57,7 @@
    2.27  done
    2.28  
    2.29  
    2.30 -subsection{*Automorphisms Form a Group*}
    2.31 +subsection\<open>Automorphisms Form a Group\<close>
    2.32  
    2.33  lemma Bij_inv_into_mem: "\<lbrakk> f \<in> Bij S;  x \<in> S\<rbrakk> \<Longrightarrow> inv_into S f x \<in> S"
    2.34  by (simp add: Bij_def bij_betw_def inv_into_into)
     3.1 --- a/src/HOL/Algebra/Congruence.thy	Sat Oct 10 16:21:34 2015 +0200
     3.2 +++ b/src/HOL/Algebra/Congruence.thy	Sat Oct 10 16:26:23 2015 +0200
     3.3 @@ -7,15 +7,15 @@
     3.4  imports Main
     3.5  begin
     3.6  
     3.7 -section {* Objects *}
     3.8 +section \<open>Objects\<close>
     3.9  
    3.10 -subsection {* Structure with Carrier Set. *}
    3.11 +subsection \<open>Structure with Carrier Set.\<close>
    3.12  
    3.13  record 'a partial_object =
    3.14    carrier :: "'a set"
    3.15  
    3.16  
    3.17 -subsection {* Structure with Carrier and Equivalence Relation @{text eq} *}
    3.18 +subsection \<open>Structure with Carrier and Equivalence Relation @{text eq}\<close>
    3.19  
    3.20  record 'a eq_object = "'a partial_object" +
    3.21    eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".=\<index>" 50)
     4.1 --- a/src/HOL/Algebra/Coset.thy	Sat Oct 10 16:21:34 2015 +0200
     4.2 +++ b/src/HOL/Algebra/Coset.thy	Sat Oct 10 16:26:23 2015 +0200
     4.3 @@ -8,7 +8,7 @@
     4.4  imports Group
     4.5  begin
     4.6  
     4.7 -section {*Cosets and Quotient Groups*}
     4.8 +section \<open>Cosets and Quotient Groups\<close>
     4.9  
    4.10  definition
    4.11    r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "#>\<index>" 60)
    4.12 @@ -39,7 +39,7 @@
    4.13    "H \<lhd> G \<equiv> normal H G"
    4.14  
    4.15  
    4.16 -subsection {*Basic Properties of Cosets*}
    4.17 +subsection \<open>Basic Properties of Cosets\<close>
    4.18  
    4.19  lemma (in group) coset_mult_assoc:
    4.20       "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
    4.21 @@ -85,7 +85,7 @@
    4.22  
    4.23  lemma (in group) coset_join2:
    4.24       "\<lbrakk>x \<in> carrier G;  subgroup H G;  x\<in>H\<rbrakk> \<Longrightarrow> H #> x = H"
    4.25 -  --{*Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.*}
    4.26 +  --\<open>Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.\<close>
    4.27  by (force simp add: subgroup.m_closed r_coset_def solve_equation)
    4.28  
    4.29  lemma (in monoid) r_coset_subset_G:
    4.30 @@ -100,7 +100,7 @@
    4.31       "\<lbrakk>H \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow> H #> x \<in> rcosets H"
    4.32  by (auto simp add: RCOSETS_def)
    4.33  
    4.34 -text{*Really needed?*}
    4.35 +text\<open>Really needed?\<close>
    4.36  lemma (in group) transpose_inv:
    4.37       "[| x \<otimes> y = z;  x \<in> carrier G;  y \<in> carrier G;  z \<in> carrier G |]
    4.38        ==> (inv x) \<otimes> z = y"
    4.39 @@ -112,7 +112,7 @@
    4.40                      subgroup.one_closed)
    4.41  done
    4.42  
    4.43 -text (in group) {* Opposite of @{thm [source] "repr_independence"} *}
    4.44 +text (in group) \<open>Opposite of @{thm [source] "repr_independence"}\<close>
    4.45  lemma (in group) repr_independenceD:
    4.46    assumes "subgroup H G"
    4.47    assumes ycarr: "y \<in> carrier G"
    4.48 @@ -127,7 +127,7 @@
    4.49    done
    4.50  qed
    4.51  
    4.52 -text {* Elements of a right coset are in the carrier *}
    4.53 +text \<open>Elements of a right coset are in the carrier\<close>
    4.54  lemma (in subgroup) elemrcos_carrier:
    4.55    assumes "group G"
    4.56    assumes acarr: "a \<in> carrier G"
    4.57 @@ -171,7 +171,7 @@
    4.58    qed
    4.59  qed
    4.60  
    4.61 -text {* Step one for lemma @{text "rcos_module"} *}
    4.62 +text \<open>Step one for lemma @{text "rcos_module"}\<close>
    4.63  lemma (in subgroup) rcos_module_imp:
    4.64    assumes "group G"
    4.65    assumes xcarr: "x \<in> carrier G"
    4.66 @@ -211,7 +211,7 @@
    4.67        show "x' \<otimes> (inv x) \<in> H" by simp
    4.68  qed
    4.69  
    4.70 -text {* Step two for lemma @{text "rcos_module"} *}
    4.71 +text \<open>Step two for lemma @{text "rcos_module"}\<close>
    4.72  lemma (in subgroup) rcos_module_rev:
    4.73    assumes "group G"
    4.74    assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
    4.75 @@ -243,7 +243,7 @@
    4.76        by fast
    4.77  qed
    4.78  
    4.79 -text {* Module property of right cosets *}
    4.80 +text \<open>Module property of right cosets\<close>
    4.81  lemma (in subgroup) rcos_module:
    4.82    assumes "group G"
    4.83    assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
    4.84 @@ -262,7 +262,7 @@
    4.85    qed
    4.86  qed
    4.87  
    4.88 -text {* Right cosets are subsets of the carrier. *} 
    4.89 +text \<open>Right cosets are subsets of the carrier.\<close> 
    4.90  lemma (in subgroup) rcosets_carrier:
    4.91    assumes "group G"
    4.92    assumes XH: "X \<in> rcosets H"
    4.93 @@ -283,7 +283,7 @@
    4.94        by (rule r_coset_subset_G)
    4.95  qed
    4.96  
    4.97 -text {* Multiplication of general subsets *}
    4.98 +text \<open>Multiplication of general subsets\<close>
    4.99  lemma (in monoid) set_mult_closed:
   4.100    assumes Acarr: "A \<subseteq> carrier G"
   4.101        and Bcarr: "B \<subseteq> carrier G"
   4.102 @@ -381,7 +381,7 @@
   4.103  qed
   4.104  
   4.105  
   4.106 -subsection {* Normal subgroups *}
   4.107 +subsection \<open>Normal subgroups\<close>
   4.108  
   4.109  lemma normal_imp_subgroup: "H \<lhd> G \<Longrightarrow> subgroup H G"
   4.110    by (simp add: normal_def subgroup_def)
   4.111 @@ -407,7 +407,7 @@
   4.112  apply (blast intro: inv_op_closed1) 
   4.113  done
   4.114  
   4.115 -text{*Alternative characterization of normal subgroups*}
   4.116 +text\<open>Alternative characterization of normal subgroups\<close>
   4.117  lemma (in group) normal_inv_iff:
   4.118       "(N \<lhd> G) = 
   4.119        (subgroup N G & (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<otimes> h \<otimes> (inv x) \<in> N))"
   4.120 @@ -456,7 +456,7 @@
   4.121  qed
   4.122  
   4.123  
   4.124 -subsection{*More Properties of Cosets*}
   4.125 +subsection\<open>More Properties of Cosets\<close>
   4.126  
   4.127  lemma (in group) lcos_m_assoc:
   4.128       "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
   4.129 @@ -524,7 +524,7 @@
   4.130  done
   4.131  
   4.132  
   4.133 -subsubsection {* Set of Inverses of an @{text r_coset}. *}
   4.134 +subsubsection \<open>Set of Inverses of an @{text r_coset}.\<close>
   4.135  
   4.136  lemma (in normal) rcos_inv:
   4.137    assumes x:     "x \<in> carrier G"
   4.138 @@ -549,7 +549,7 @@
   4.139  qed
   4.140  
   4.141  
   4.142 -subsubsection {*Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.*}
   4.143 +subsubsection \<open>Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.\<close>
   4.144  
   4.145  lemma (in group) setmult_rcos_assoc:
   4.146       "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
   4.147 @@ -584,12 +584,12 @@
   4.148  by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
   4.149  
   4.150  lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
   4.151 -  -- {* generalizes @{text subgroup_mult_id} *}
   4.152 +  -- \<open>generalizes @{text subgroup_mult_id}\<close>
   4.153    by (auto simp add: RCOSETS_def subset
   4.154          setmult_rcos_assoc subgroup_mult_id normal.axioms normal_axioms)
   4.155  
   4.156  
   4.157 -subsubsection{*An Equivalence Relation*}
   4.158 +subsubsection\<open>An Equivalence Relation\<close>
   4.159  
   4.160  definition
   4.161    r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set"  ("rcong\<index> _")
   4.162 @@ -628,9 +628,9 @@
   4.163    qed
   4.164  qed
   4.165  
   4.166 -text{*Equivalence classes of @{text rcong} correspond to left cosets.
   4.167 +text\<open>Equivalence classes of @{text rcong} correspond to left cosets.
   4.168    Was there a mistake in the definitions? I'd have expected them to
   4.169 -  correspond to right cosets.*}
   4.170 +  correspond to right cosets.\<close>
   4.171  
   4.172  (* CB: This is correct, but subtle.
   4.173     We call H #> a the right coset of a relative to H.  According to
   4.174 @@ -652,7 +652,7 @@
   4.175  qed
   4.176  
   4.177  
   4.178 -subsubsection{*Two Distinct Right Cosets are Disjoint*}
   4.179 +subsubsection\<open>Two Distinct Right Cosets are Disjoint\<close>
   4.180  
   4.181  lemma (in group) rcos_equation:
   4.182    assumes "subgroup H G"
   4.183 @@ -679,9 +679,9 @@
   4.184  qed
   4.185  
   4.186  
   4.187 -subsection {* Further lemmas for @{text "r_congruent"} *}
   4.188 +subsection \<open>Further lemmas for @{text "r_congruent"}\<close>
   4.189  
   4.190 -text {* The relation is a congruence *}
   4.191 +text \<open>The relation is a congruence\<close>
   4.192  
   4.193  lemma (in normal) congruent_rcong:
   4.194    shows "congruent2 (rcong H) (rcong H) (\<lambda>a b. a \<otimes> b <# H)"
   4.195 @@ -753,7 +753,7 @@
   4.196  qed
   4.197  
   4.198  
   4.199 -subsection {*Order of a Group and Lagrange's Theorem*}
   4.200 +subsection \<open>Order of a Group and Lagrange's Theorem\<close>
   4.201  
   4.202  definition
   4.203    order :: "('a, 'b) monoid_scheme \<Rightarrow> nat"
   4.204 @@ -777,7 +777,7 @@
   4.205  apply (simp add: r_coset_subset_G [THEN finite_subset])
   4.206  done
   4.207  
   4.208 -text{*The next two lemmas support the proof of @{text card_cosets_equal}.*}
   4.209 +text\<open>The next two lemmas support the proof of @{text card_cosets_equal}.\<close>
   4.210  lemma (in group) inj_on_f:
   4.211      "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
   4.212  apply (rule inj_onI)
   4.213 @@ -799,7 +799,7 @@
   4.214      apply (force simp add: m_assoc subsetD r_coset_def)
   4.215     apply (rule inj_on_g, assumption+)
   4.216    apply (force simp add: m_assoc subsetD r_coset_def)
   4.217 - txt{*The sets @{term "H #> a"} and @{term "H"} are finite.*}
   4.218 + txt\<open>The sets @{term "H #> a"} and @{term "H"} are finite.\<close>
   4.219   apply (simp add: r_coset_subset_G [THEN finite_subset])
   4.220  apply (blast intro: finite_subset)
   4.221  done
   4.222 @@ -824,11 +824,11 @@
   4.223  done
   4.224  
   4.225  
   4.226 -subsection {*Quotient Groups: Factorization of a Group*}
   4.227 +subsection \<open>Quotient Groups: Factorization of a Group\<close>
   4.228  
   4.229  definition
   4.230    FactGroup :: "[('a,'b) monoid_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "Mod" 65)
   4.231 -    --{*Actually defined for groups rather than monoids*}
   4.232 +    --\<open>Actually defined for groups rather than monoids\<close>
   4.233     where "FactGroup G H = \<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
   4.234  
   4.235  lemma (in normal) setmult_closed:
   4.236 @@ -880,21 +880,21 @@
   4.237  apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
   4.238  done
   4.239  
   4.240 -text{*The coset map is a homomorphism from @{term G} to the quotient group
   4.241 -  @{term "G Mod H"}*}
   4.242 +text\<open>The coset map is a homomorphism from @{term G} to the quotient group
   4.243 +  @{term "G Mod H"}\<close>
   4.244  lemma (in normal) r_coset_hom_Mod:
   4.245    "(\<lambda>a. H #> a) \<in> hom G (G Mod H)"
   4.246    by (auto simp add: FactGroup_def RCOSETS_def Pi_def hom_def rcos_sum)
   4.247  
   4.248   
   4.249 -subsection{*The First Isomorphism Theorem*}
   4.250 +subsection\<open>The First Isomorphism Theorem\<close>
   4.251  
   4.252 -text{*The quotient by the kernel of a homomorphism is isomorphic to the 
   4.253 -  range of that homomorphism.*}
   4.254 +text\<open>The quotient by the kernel of a homomorphism is isomorphic to the 
   4.255 +  range of that homomorphism.\<close>
   4.256  
   4.257  definition
   4.258    kernel :: "('a, 'm) monoid_scheme \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow>  ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
   4.259 -    --{*the kernel of a homomorphism*}
   4.260 +    --\<open>the kernel of a homomorphism\<close>
   4.261    where "kernel G H h = {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}"
   4.262  
   4.263  lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
   4.264 @@ -902,7 +902,7 @@
   4.265  apply (auto simp add: kernel_def group.intro is_group) 
   4.266  done
   4.267  
   4.268 -text{*The kernel of a homomorphism is a normal subgroup*}
   4.269 +text\<open>The kernel of a homomorphism is a normal subgroup\<close>
   4.270  lemma (in group_hom) normal_kernel: "(kernel G H h) \<lhd> G"
   4.271  apply (simp add: G.normal_inv_iff subgroup_kernel)
   4.272  apply (simp add: kernel_def)
   4.273 @@ -957,7 +957,7 @@
   4.274  qed
   4.275  
   4.276  
   4.277 -text{*Lemma for the following injectivity result*}
   4.278 +text\<open>Lemma for the following injectivity result\<close>
   4.279  lemma (in group_hom) FactGroup_subset:
   4.280       "\<lbrakk>g \<in> carrier G; g' \<in> carrier G; h g = h g'\<rbrakk>
   4.281        \<Longrightarrow>  kernel G H h #> g \<subseteq> kernel G H h #> g'"
   4.282 @@ -986,8 +986,8 @@
   4.283    show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX) 
   4.284  qed
   4.285  
   4.286 -text{*If the homomorphism @{term h} is onto @{term H}, then so is the
   4.287 -homomorphism from the quotient group*}
   4.288 +text\<open>If the homomorphism @{term h} is onto @{term H}, then so is the
   4.289 +homomorphism from the quotient group\<close>
   4.290  lemma (in group_hom) FactGroup_onto:
   4.291    assumes h: "h ` carrier G = carrier H"
   4.292    shows "(\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
   4.293 @@ -1008,8 +1008,8 @@
   4.294  qed
   4.295  
   4.296  
   4.297 -text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
   4.298 - quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
   4.299 +text\<open>If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
   4.300 + quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.\<close>
   4.301  theorem (in group_hom) FactGroup_iso:
   4.302    "h ` carrier G = carrier H
   4.303     \<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
     5.1 --- a/src/HOL/Algebra/Divisibility.thy	Sat Oct 10 16:21:34 2015 +0200
     5.2 +++ b/src/HOL/Algebra/Divisibility.thy	Sat Oct 10 16:26:23 2015 +0200
     5.3 @@ -3,15 +3,15 @@
     5.4      Author:     Stephan Hohe
     5.5  *)
     5.6  
     5.7 -section {* Divisibility in monoids and rings *}
     5.8 +section \<open>Divisibility in monoids and rings\<close>
     5.9  
    5.10  theory Divisibility
    5.11  imports "~~/src/HOL/Library/Permutation" Coset Group
    5.12  begin
    5.13  
    5.14 -section {* Factorial Monoids *}
    5.15 -
    5.16 -subsection {* Monoids with Cancellation Law *}
    5.17 +section \<open>Factorial Monoids\<close>
    5.18 +
    5.19 +subsection \<open>Monoids with Cancellation Law\<close>
    5.20  
    5.21  locale monoid_cancel = monoid +
    5.22    assumes l_cancel: 
    5.23 @@ -57,7 +57,7 @@
    5.24    ..
    5.25  
    5.26  
    5.27 -subsection {* Products of Units in Monoids *}
    5.28 +subsection \<open>Products of Units in Monoids\<close>
    5.29  
    5.30  lemma (in monoid) Units_m_closed[simp, intro]:
    5.31    assumes h1unit: "h1 \<in> Units G" and h2unit: "h2 \<in> Units G"
    5.32 @@ -144,9 +144,9 @@
    5.33  qed
    5.34  
    5.35  
    5.36 -subsection {* Divisibility and Association *}
    5.37 -
    5.38 -subsubsection {* Function definitions *}
    5.39 +subsection \<open>Divisibility and Association\<close>
    5.40 +
    5.41 +subsubsection \<open>Function definitions\<close>
    5.42  
    5.43  definition
    5.44    factor :: "[_, 'a, 'a] \<Rightarrow> bool" (infix "divides\<index>" 65)
    5.45 @@ -174,7 +174,7 @@
    5.46      (\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. p divides\<^bsub>G\<^esub> (a \<otimes>\<^bsub>G\<^esub> b) \<longrightarrow> p divides\<^bsub>G\<^esub> a \<or> p divides\<^bsub>G\<^esub> b)"
    5.47  
    5.48  
    5.49 -subsubsection {* Divisibility *}
    5.50 +subsubsection \<open>Divisibility\<close>
    5.51  
    5.52  lemma dividesI:
    5.53    fixes G (structure)
    5.54 @@ -309,7 +309,7 @@
    5.55  by (fast dest: divides_unit intro: unit_divides)
    5.56  
    5.57  
    5.58 -subsubsection {* Association *}
    5.59 +subsubsection \<open>Association\<close>
    5.60  
    5.61  lemma associatedI:
    5.62    fixes G (structure)
    5.63 @@ -449,7 +449,7 @@
    5.64    done
    5.65  
    5.66  
    5.67 -subsubsection {* Division and associativity *}
    5.68 +subsubsection \<open>Division and associativity\<close>
    5.69  
    5.70  lemma divides_antisym:
    5.71    fixes G (structure)
    5.72 @@ -497,7 +497,7 @@
    5.73    done
    5.74  
    5.75      
    5.76 -subsubsection {* Multiplication and associativity *}
    5.77 +subsubsection \<open>Multiplication and associativity\<close>
    5.78  
    5.79  lemma (in monoid_cancel) mult_cong_r:
    5.80    assumes "b \<sim> b'"
    5.81 @@ -545,7 +545,7 @@
    5.82  done
    5.83  
    5.84  
    5.85 -subsubsection {* Units *}
    5.86 +subsubsection \<open>Units\<close>
    5.87  
    5.88  lemma (in monoid_cancel) assoc_unit_l [trans]:
    5.89    assumes asc: "a \<sim> b" and bunit: "b \<in> Units G"
    5.90 @@ -604,7 +604,7 @@
    5.91  done
    5.92  
    5.93  
    5.94 -subsubsection {* Proper factors *}
    5.95 +subsubsection \<open>Proper factors\<close>
    5.96  
    5.97  lemma properfactorI:
    5.98    fixes G (structure)
    5.99 @@ -785,9 +785,9 @@
   5.100  by (intro properfactor_trans2[OF ab] divides_prod_l, simp+)
   5.101  
   5.102  
   5.103 -subsection {* Irreducible Elements and Primes *}
   5.104 -
   5.105 -subsubsection {* Irreducible elements *}
   5.106 +subsection \<open>Irreducible Elements and Primes\<close>
   5.107 +
   5.108 +subsubsection \<open>Irreducible elements\<close>
   5.109  
   5.110  lemma irreducibleI:
   5.111    fixes G (structure)
   5.112 @@ -903,7 +903,7 @@
   5.113  qed
   5.114  
   5.115  
   5.116 -subsubsection {* Prime elements *}
   5.117 +subsubsection \<open>Prime elements\<close>
   5.118  
   5.119  lemma primeI:
   5.120    fixes G (structure)
   5.121 @@ -943,9 +943,9 @@
   5.122  apply (metis assms(2) assms(3) assms(4) associated_sym divides_cong_l m_closed)
   5.123  done
   5.124  
   5.125 -subsection {* Factorization and Factorial Monoids *}
   5.126 -
   5.127 -subsubsection {* Function definitions *}
   5.128 +subsection \<open>Factorization and Factorial Monoids\<close>
   5.129 +
   5.130 +subsubsection \<open>Function definitions\<close>
   5.131  
   5.132  definition
   5.133    factors :: "[_, 'a list, 'a] \<Rightarrow> bool"
   5.134 @@ -972,9 +972,9 @@
   5.135              set fs \<subseteq> carrier G; set fs' \<subseteq> carrier G\<rbrakk> \<Longrightarrow> essentially_equal G fs fs'"
   5.136  
   5.137  
   5.138 -subsubsection {* Comparing lists of elements *}
   5.139 -
   5.140 -text {* Association on lists *}
   5.141 +subsubsection \<open>Comparing lists of elements\<close>
   5.142 +
   5.143 +text \<open>Association on lists\<close>
   5.144  
   5.145  lemma (in monoid) listassoc_refl [simp, intro]:
   5.146    assumes "set as \<subseteq> carrier G"
   5.147 @@ -1019,7 +1019,7 @@
   5.148  done
   5.149  
   5.150  
   5.151 -text {* Permutations *}
   5.152 +text \<open>Permutations\<close>
   5.153  
   5.154  lemma perm_map [intro]:
   5.155    assumes p: "a <~~> b"
   5.156 @@ -1077,7 +1077,7 @@
   5.157      perm_setP[of _ _ "\<lambda>as. \<forall>a\<in>as. irreducible G a"]
   5.158  
   5.159  
   5.160 -text {* Essentially equal factorizations *}
   5.161 +text \<open>Essentially equal factorizations\<close>
   5.162  
   5.163  lemma (in monoid) essentially_equalI:
   5.164    assumes ex: "fs1 <~~> fs1'"  "fs1' [\<sim>] fs2"
   5.165 @@ -1149,9 +1149,9 @@
   5.166  qed
   5.167  
   5.168  
   5.169 -subsubsection {* Properties of lists of elements *}
   5.170 -
   5.171 -text {* Multiplication of factors in a list *}
   5.172 +subsubsection \<open>Properties of lists of elements\<close>
   5.173 +
   5.174 +text \<open>Multiplication of factors in a list\<close>
   5.175  
   5.176  lemma (in monoid) multlist_closed [simp, intro]:
   5.177    assumes ascarr: "set fs \<subseteq> carrier G"
   5.178 @@ -1224,7 +1224,7 @@
   5.179  done
   5.180  
   5.181  
   5.182 -subsubsection {* Factorization in irreducible elements *}
   5.183 +subsubsection \<open>Factorization in irreducible elements\<close>
   5.184  
   5.185  lemma wfactorsI:
   5.186    fixes G (structure)
   5.187 @@ -1328,7 +1328,7 @@
   5.188  qed
   5.189  
   5.190  
   5.191 -text {* Comparing wfactors *}
   5.192 +text \<open>Comparing wfactors\<close>
   5.193  
   5.194  lemma (in comm_monoid_cancel) wfactors_listassoc_cong_l:
   5.195    assumes fact: "wfactors G fs a"
   5.196 @@ -1389,7 +1389,7 @@
   5.197  qed
   5.198  
   5.199  
   5.200 -subsubsection {* Essentially equal factorizations *}
   5.201 +subsubsection \<open>Essentially equal factorizations\<close>
   5.202  
   5.203  lemma (in comm_monoid_cancel) unitfactor_ee:
   5.204    assumes uunit: "u \<in> Units G"
   5.205 @@ -1719,7 +1719,7 @@
   5.206  qed
   5.207  
   5.208  
   5.209 -subsubsection {* Factorial monoids and wfactors *}
   5.210 +subsubsection \<open>Factorial monoids and wfactors\<close>
   5.211  
   5.212  lemma (in comm_monoid_cancel) factorial_monoidI:
   5.213    assumes wfactors_exists: 
   5.214 @@ -1782,9 +1782,9 @@
   5.215  qed (blast intro: factors_wfactors wfactors_unique)
   5.216  
   5.217  
   5.218 -subsection {* Factorizations as Multisets *}
   5.219 -
   5.220 -text {* Gives useful operations like intersection *}
   5.221 +subsection \<open>Factorizations as Multisets\<close>
   5.222 +
   5.223 +text \<open>Gives useful operations like intersection\<close>
   5.224  
   5.225  (* FIXME: use class_of x instead of closure_of {x} *)
   5.226  
   5.227 @@ -1795,7 +1795,7 @@
   5.228    "fmset G as = mset (map (\<lambda>a. assocs G a) as)"
   5.229  
   5.230  
   5.231 -text {* Helper lemmas *}
   5.232 +text \<open>Helper lemmas\<close>
   5.233  
   5.234  lemma (in monoid) assocs_repr_independence:
   5.235    assumes "y \<in> assocs G x"
   5.236 @@ -1834,7 +1834,7 @@
   5.237      assocs_repr_independenceD[THEN assocs_assoc]
   5.238  
   5.239  
   5.240 -subsubsection {* Comparing multisets *}
   5.241 +subsubsection \<open>Comparing multisets\<close>
   5.242  
   5.243  lemma (in monoid) fmset_perm_cong:
   5.244    assumes prm: "as <~~> bs"
   5.245 @@ -2022,7 +2022,7 @@
   5.246  by (fast intro: ee_fmset fmset_ee)
   5.247  
   5.248  
   5.249 -subsubsection {* Interpreting multisets as factorizations *}
   5.250 +subsubsection \<open>Interpreting multisets as factorizations\<close>
   5.251  
   5.252  lemma (in monoid) mset_fmsetEx:
   5.253    assumes elems: "\<And>X. X \<in> set_mset Cs \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"
   5.254 @@ -2089,7 +2089,7 @@
   5.255  qed
   5.256  
   5.257  
   5.258 -subsubsection {* Multiplication on multisets *}
   5.259 +subsubsection \<open>Multiplication on multisets\<close>
   5.260  
   5.261  lemma (in factorial_monoid) mult_wfactors_fmset:
   5.262    assumes afs: "wfactors G as a" and bfs: "wfactors G bs b" and cfs: "wfactors G cs (a \<otimes> b)"
   5.263 @@ -2131,7 +2131,7 @@
   5.264  qed
   5.265  
   5.266  
   5.267 -subsubsection {* Divisibility on multisets *}
   5.268 +subsubsection \<open>Divisibility on multisets\<close>
   5.269  
   5.270  lemma (in factorial_monoid) divides_fmsubset:
   5.271    assumes ab: "a divides b"
   5.272 @@ -2215,7 +2215,7 @@
   5.273  by (blast intro: divides_fmsubset fmsubset_divides)
   5.274  
   5.275  
   5.276 -text {* Proper factors on multisets *}
   5.277 +text \<open>Proper factors on multisets\<close>
   5.278  
   5.279  lemma (in factorial_monoid) fmset_properfactor:
   5.280    assumes asubb: "fmset G as \<le># fmset G bs"
   5.281 @@ -2250,7 +2250,7 @@
   5.282  apply (metis assms divides_fmsubset fmsubset_divides)
   5.283  done
   5.284  
   5.285 -subsection {* Irreducible Elements are Prime *}
   5.286 +subsection \<open>Irreducible Elements are Prime\<close>
   5.287  
   5.288  lemma (in factorial_monoid) irreducible_is_prime:
   5.289    assumes pirr: "irreducible G p"
   5.290 @@ -2490,9 +2490,9 @@
   5.291  qed
   5.292  
   5.293  
   5.294 -subsection {* Greatest Common Divisors and Lowest Common Multiples *}
   5.295 -
   5.296 -subsubsection {* Definitions *}
   5.297 +subsection \<open>Greatest Common Divisors and Lowest Common Multiples\<close>
   5.298 +
   5.299 +subsubsection \<open>Definitions\<close>
   5.300  
   5.301  definition
   5.302    isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \<Rightarrow> bool"  ("(_ gcdof\<index> _ _)" [81,81,81] 80)
   5.303 @@ -2529,7 +2529,7 @@
   5.304            "wf {(x, y). x \<in> carrier G \<and> y \<in> carrier G \<and> properfactor G x y}"
   5.305  
   5.306  
   5.307 -subsubsection {* Connections to \texttt{Lattice.thy} *}
   5.308 +subsubsection \<open>Connections to \texttt{Lattice.thy}\<close>
   5.309  
   5.310  lemma gcdof_greatestLower:
   5.311    fixes G (structure)
   5.312 @@ -2571,7 +2571,7 @@
   5.313  by fast
   5.314  
   5.315  
   5.316 -subsubsection {* Existence of gcd and lcm *}
   5.317 +subsubsection \<open>Existence of gcd and lcm\<close>
   5.318  
   5.319  lemma (in factorial_monoid) gcdof_exists:
   5.320    assumes acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
   5.321 @@ -2753,9 +2753,9 @@
   5.322  qed
   5.323  
   5.324  
   5.325 -subsection {* Conditions for Factoriality *}
   5.326 -
   5.327 -subsubsection {* Gcd condition *}
   5.328 +subsection \<open>Conditions for Factoriality\<close>
   5.329 +
   5.330 +subsubsection \<open>Gcd condition\<close>
   5.331  
   5.332  lemma (in gcd_condition_monoid) division_weak_lower_semilattice [simp]:
   5.333    shows "weak_lower_semilattice (division_rel G)"
   5.334 @@ -3153,7 +3153,7 @@
   5.335    by (rule primeness_condition)
   5.336  
   5.337  
   5.338 -subsubsection {* Divisor chain condition *}
   5.339 +subsubsection \<open>Divisor chain condition\<close>
   5.340  
   5.341  lemma (in divisor_chain_condition_monoid) wfactors_exist:
   5.342    assumes acarr: "a \<in> carrier G"
   5.343 @@ -3243,7 +3243,7 @@
   5.344  qed
   5.345  
   5.346  
   5.347 -subsubsection {* Primeness condition *}
   5.348 +subsubsection \<open>Primeness condition\<close>
   5.349  
   5.350  lemma (in comm_monoid_cancel) multlist_prime_pos:
   5.351    assumes carr: "a \<in> carrier G"  "set as \<subseteq> carrier G"
   5.352 @@ -3481,9 +3481,9 @@
   5.353  done
   5.354  
   5.355  
   5.356 -subsubsection {* Application to factorial monoids *}
   5.357 -
   5.358 -text {* Number of factors for wellfoundedness *}
   5.359 +subsubsection \<open>Application to factorial monoids\<close>
   5.360 +
   5.361 +text \<open>Number of factors for wellfoundedness\<close>
   5.362  
   5.363  definition
   5.364    factorcount :: "_ \<Rightarrow> 'a \<Rightarrow> nat" where
   5.365 @@ -3678,7 +3678,7 @@
   5.366  qed
   5.367  
   5.368  
   5.369 -subsection {* Factoriality Theorems *}
   5.370 +subsection \<open>Factoriality Theorems\<close>
   5.371  
   5.372  theorem factorial_condition_one: (* Jacobson theorem 2.21 *)
   5.373    shows "(divisor_chain_condition_monoid G \<and> primeness_condition_monoid G) = 
     6.1 --- a/src/HOL/Algebra/Exponent.thy	Sat Oct 10 16:21:34 2015 +0200
     6.2 +++ b/src/HOL/Algebra/Exponent.thy	Sat Oct 10 16:26:23 2015 +0200
     6.3 @@ -9,16 +9,16 @@
     6.4  imports Main "~~/src/HOL/Number_Theory/Primes"
     6.5  begin
     6.6  
     6.7 -section {*Sylow's Theorem*}
     6.8 +section \<open>Sylow's Theorem\<close>
     6.9  
    6.10 -subsection {*The Combinatorial Argument Underlying the First Sylow Theorem*}
    6.11 +subsection \<open>The Combinatorial Argument Underlying the First Sylow Theorem\<close>
    6.12  
    6.13  definition
    6.14    exponent :: "nat => nat => nat"
    6.15    where "exponent p s = (if prime p then (GREATEST r. p^r dvd s) else 0)"
    6.16  
    6.17  
    6.18 -text{*Prime Theorems*}
    6.19 +text\<open>Prime Theorems\<close>
    6.20  
    6.21  lemma prime_iff:
    6.22    "(prime p) = (Suc 0 < p & (\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))"
    6.23 @@ -100,7 +100,7 @@
    6.24  done
    6.25  
    6.26  
    6.27 -text{*Exponent Theorems*}
    6.28 +text\<open>Exponent Theorems\<close>
    6.29  
    6.30  lemma exponent_ge [rule_format]:
    6.31    "[|p^k dvd n;  prime p;  0<n|] ==> k <= exponent p n"
    6.32 @@ -182,7 +182,7 @@
    6.33  done
    6.34  
    6.35  
    6.36 -text{*Main Combinatorial Argument*}
    6.37 +text\<open>Main Combinatorial Argument\<close>
    6.38  
    6.39  lemma gcd_mult': fixes a::nat shows "gcd b (a * b) = b"
    6.40  by (simp add: mult.commute[of a b])
    6.41 @@ -236,7 +236,7 @@
    6.42  apply (blast intro: exponent_equalityI p_fac_forw p_fac_backw)
    6.43  done
    6.44  
    6.45 -text{*Suc rules that we have to delete from the simpset*}
    6.46 +text\<open>Suc rules that we have to delete from the simpset\<close>
    6.47  lemmas bad_Sucs = binomial_Suc_Suc mult_Suc mult_Suc_right
    6.48  
    6.49  (*The bound K is needed; otherwise it's too weak to be used.*)
    6.50 @@ -252,9 +252,9 @@
    6.51   prefer 2 apply (simp, clarify)
    6.52  apply (subgoal_tac "exponent p ((Suc (j+k) choose Suc k) * Suc k) =
    6.53                      exponent p (Suc k)")
    6.54 - txt{*First, use the assumed equation.  We simplify the LHS to
    6.55 + txt\<open>First, use the assumed equation.  We simplify the LHS to
    6.56    @{term "exponent p (Suc (j + k) choose Suc k) + exponent p (Suc k)"}
    6.57 -  the common terms cancel, proving the conclusion.*}
    6.58 +  the common terms cancel, proving the conclusion.\<close>
    6.59   apply (simp del: bad_Sucs add: exponent_mult_add)
    6.60  apply (simp del: bad_Sucs add: mult_ac Suc_times_binomial exponent_mult_add)
    6.61  
    6.62 @@ -297,14 +297,14 @@
    6.63   prefer 2 apply simp
    6.64  apply (subgoal_tac "0 < p^a * m & p^a <= p^a * m")
    6.65   prefer 2 apply (force simp add: prime_iff)
    6.66 -txt{*A similar trick to the one used in @{text p_not_div_choose_lemma}:
    6.67 +txt\<open>A similar trick to the one used in @{text p_not_div_choose_lemma}:
    6.68    insert an equation; use @{text exponent_mult_add} on the LHS; on the RHS,
    6.69    first
    6.70 -  transform the binomial coefficient, then use @{text exponent_mult_add}.*}
    6.71 +  transform the binomial coefficient, then use @{text exponent_mult_add}.\<close>
    6.72  apply (subgoal_tac "exponent p ((( (p^a) * m) choose p^a) * p^a) =
    6.73                      a + exponent p m")
    6.74   apply (simp add: exponent_mult_add)
    6.75 -txt{*one subgoal left!*}
    6.76 +txt\<open>one subgoal left!\<close>
    6.77  apply (auto simp: mult_ac)
    6.78  apply (subst times_binomial_minus1_eq, simp)
    6.79  apply (simp add: diff_le_mono exponent_mult_add)
     7.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Sat Oct 10 16:21:34 2015 +0200
     7.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Sat Oct 10 16:26:23 2015 +0200
     7.3 @@ -8,14 +8,14 @@
     7.4  imports Group
     7.5  begin
     7.6  
     7.7 -subsection {* Product Operator for Commutative Monoids *}
     7.8 +subsection \<open>Product Operator for Commutative Monoids\<close>
     7.9  
    7.10 -subsubsection {* Inductive Definition of a Relation for Products over Sets *}
    7.11 +subsubsection \<open>Inductive Definition of a Relation for Products over Sets\<close>
    7.12  
    7.13 -text {* Instantiation of locale @{text LC} of theory @{text Finite_Set} is not
    7.14 +text \<open>Instantiation of locale @{text LC} of theory @{text Finite_Set} is not
    7.15    possible, because here we have explicit typing rules like 
    7.16    @{text "x \<in> carrier G"}.  We introduce an explicit argument for the domain
    7.17 -  @{text D}. *}
    7.18 +  @{text D}.\<close>
    7.19  
    7.20  inductive_set
    7.21    foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set"
    7.22 @@ -61,7 +61,7 @@
    7.23  qed
    7.24  
    7.25  
    7.26 -text {* Left-Commutative Operations *}
    7.27 +text \<open>Left-Commutative Operations\<close>
    7.28  
    7.29  locale LCD =
    7.30    fixes B :: "'b set"
    7.31 @@ -111,7 +111,7 @@
    7.32    apply (erule foldSetD.cases)
    7.33     apply blast
    7.34    apply clarify
    7.35 -  txt {* force simplification of @{text "card A < card (insert ...)"}. *}
    7.36 +  txt \<open>force simplification of @{text "card A < card (insert ...)"}.\<close>
    7.37    apply (erule rev_mp)
    7.38    apply (simp add: less_Suc_eq_le)
    7.39    apply (rule impI)
    7.40 @@ -119,7 +119,7 @@
    7.41     apply (subgoal_tac "Aa = Ab")
    7.42      prefer 2 apply (blast elim!: equalityE)
    7.43     apply blast
    7.44 -  txt {* case @{prop "xa \<notin> xb"}. *}
    7.45 +  txt \<open>case @{prop "xa \<notin> xb"}.\<close>
    7.46    apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb \<in> Aa & xa \<in> Ab")
    7.47     prefer 2 apply (blast elim!: equalityE)
    7.48    apply clarify
    7.49 @@ -221,7 +221,7 @@
    7.50      ==> foldD D f e (A Un B) = foldD D f (foldD D f e B) A"
    7.51    by (simp add: foldD_nest_Un_Int)
    7.52  
    7.53 --- {* Delete rules to do with @{text foldSetD} relation. *}
    7.54 +-- \<open>Delete rules to do with @{text foldSetD} relation.\<close>
    7.55  
    7.56  declare foldSetD_imp_finite [simp del]
    7.57    empty_foldSetDE [rule del]
    7.58 @@ -230,12 +230,12 @@
    7.59    foldSetD_closed [rule del]
    7.60  
    7.61  
    7.62 -text {* Commutative Monoids *}
    7.63 +text \<open>Commutative Monoids\<close>
    7.64  
    7.65 -text {*
    7.66 +text \<open>
    7.67    We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
    7.68    instead of @{text "'b => 'a => 'a"}.
    7.69 -*}
    7.70 +\<close>
    7.71  
    7.72  locale ACeD =
    7.73    fixes D :: "'a set"
    7.74 @@ -263,7 +263,7 @@
    7.75  proof -
    7.76    assume "x \<in> D"
    7.77    then have "x \<cdot> e = x" by (rule ident)
    7.78 -  with `x \<in> D` show ?thesis by (simp add: commute)
    7.79 +  with \<open>x \<in> D\<close> show ?thesis by (simp add: commute)
    7.80  qed
    7.81  
    7.82  lemma (in ACeD) foldD_Un_Int:
    7.83 @@ -285,7 +285,7 @@
    7.84      left_commute LCD.foldD_closed [OF LCD.intro [of D]])
    7.85  
    7.86  
    7.87 -subsubsection {* Products over Finite Sets *}
    7.88 +subsubsection \<open>Products over Finite Sets\<close>
    7.89  
    7.90  definition
    7.91    finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
    7.92 @@ -299,7 +299,7 @@
    7.93        ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
    7.94  translations
    7.95    "\<Otimes>\<index>i\<in>A. b" \<rightleftharpoons> "CONST finprod \<struct>\<index> (%i. b) A"
    7.96 -  -- {* Beware of argument permutation! *}
    7.97 +  -- \<open>Beware of argument permutation!\<close>
    7.98  
    7.99  lemma (in comm_monoid) finprod_empty [simp]: 
   7.100    "finprod G f {} = \<one>"
   7.101 @@ -367,7 +367,7 @@
   7.102    "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
   7.103       finprod G g (A Un B) \<otimes> finprod G g (A Int B) =
   7.104       finprod G g A \<otimes> finprod G g B"
   7.105 --- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   7.106 +-- \<open>The reversed orientation looks more natural, but LOOPS as a simprule!\<close>
   7.107  proof (induct set: finite)
   7.108    case empty then show ?case by simp
   7.109  next
   7.110 @@ -450,12 +450,12 @@
   7.111    (* This order of prems is slightly faster (3%) than the last two swapped. *)
   7.112    by (rule finprod_cong') (auto simp add: simp_implies_def)
   7.113  
   7.114 -text {*Usually, if this rule causes a failed congruence proof error,
   7.115 +text \<open>Usually, if this rule causes a failed congruence proof error,
   7.116    the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
   7.117    Adding @{thm [source] Pi_def} to the simpset is often useful.
   7.118    For this reason, @{thm [source] finprod_cong}
   7.119    is not added to the simpset by default.
   7.120 -*}
   7.121 +\<close>
   7.122  
   7.123  end
   7.124  
   7.125 @@ -497,7 +497,7 @@
   7.126    case (infinite A)
   7.127    hence "\<not> finite (h ` A)"
   7.128      using finite_imageD by blast
   7.129 -  with `\<not> finite A` show ?case by simp
   7.130 +  with \<open>\<not> finite A\<close> show ?case by simp
   7.131  qed (auto simp add: Pi_def)
   7.132  
   7.133  lemma finprod_const:
     8.1 --- a/src/HOL/Algebra/Group.thy	Sat Oct 10 16:21:34 2015 +0200
     8.2 +++ b/src/HOL/Algebra/Group.thy	Sat Oct 10 16:26:23 2015 +0200
     8.3 @@ -8,13 +8,13 @@
     8.4  imports Lattice "~~/src/HOL/Library/FuncSet"
     8.5  begin
     8.6  
     8.7 -section {* Monoids and Groups *}
     8.8 +section \<open>Monoids and Groups\<close>
     8.9  
    8.10 -subsection {* Definitions *}
    8.11 +subsection \<open>Definitions\<close>
    8.12  
    8.13 -text {*
    8.14 +text \<open>
    8.15    Definitions follow @{cite "Jacobson:1985"}.
    8.16 -*}
    8.17 +\<close>
    8.18  
    8.19  record 'a monoid =  "'a partial_object" +
    8.20    mult    :: "['a, 'a] \<Rightarrow> 'a" (infixl "\<otimes>\<index>" 70)
    8.21 @@ -26,7 +26,7 @@
    8.22  
    8.23  definition
    8.24    Units :: "_ => 'a set"
    8.25 -  --{*The set of invertible elements*}
    8.26 +  --\<open>The set of invertible elements\<close>
    8.27    where "Units G = {y. y \<in> carrier G & (\<exists>x \<in> carrier G. x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> & y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)}"
    8.28  
    8.29  consts
    8.30 @@ -187,7 +187,7 @@
    8.31    with G show ?thesis by (simp del: r_one add: m_assoc Units_closed)
    8.32  qed
    8.33  
    8.34 -text {* Power *}
    8.35 +text \<open>Power\<close>
    8.36  
    8.37  lemma (in monoid) nat_pow_closed [intro, simp]:
    8.38    "x \<in> carrier G ==> x (^) (n::nat) \<in> carrier G"
    8.39 @@ -218,11 +218,11 @@
    8.40  (* Jacobson defines the order of a monoid here. *)
    8.41  
    8.42  
    8.43 -subsection {* Groups *}
    8.44 +subsection \<open>Groups\<close>
    8.45  
    8.46 -text {*
    8.47 +text \<open>
    8.48    A group is a monoid all of whose elements are invertible.
    8.49 -*}
    8.50 +\<close>
    8.51  
    8.52  locale group = monoid +
    8.53    assumes Units: "carrier G <= Units G"
    8.54 @@ -321,7 +321,7 @@
    8.55    using Units_l_inv by simp
    8.56  
    8.57  
    8.58 -subsection {* Cancellation Laws and Basic Properties *}
    8.59 +subsection \<open>Cancellation Laws and Basic Properties\<close>
    8.60  
    8.61  lemma (in group) l_cancel [simp]:
    8.62    "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    8.63 @@ -397,7 +397,7 @@
    8.64    "\<lbrakk> a \<in> carrier G; b \<in> carrier G; c \<in> carrier G \<rbrakk> \<Longrightarrow> a = b \<otimes> inv c \<longleftrightarrow> b = a \<otimes> c"
    8.65    by (metis inv_equality l_inv_ex l_one m_assoc r_inv)
    8.66  
    8.67 -text {* Power *}
    8.68 +text \<open>Power\<close>
    8.69  
    8.70  lemma (in group) int_pow_def2:
    8.71    "a (^) (z::int) = (if z < 0 then inv (a (^) (nat (-z))) else a (^) (nat z))"
    8.72 @@ -435,7 +435,7 @@
    8.73  qed
    8.74  
    8.75   
    8.76 -subsection {* Subgroups *}
    8.77 +subsection \<open>Subgroups\<close>
    8.78  
    8.79  locale subgroup =
    8.80    fixes H and G (structure)
    8.81 @@ -469,18 +469,18 @@
    8.82      done
    8.83  qed
    8.84  
    8.85 -text {*
    8.86 +text \<open>
    8.87    Since @{term H} is nonempty, it contains some element @{term x}.  Since
    8.88    it is closed under inverse, it contains @{text "inv x"}.  Since
    8.89    it is closed under product, it contains @{text "x \<otimes> inv x = \<one>"}.
    8.90 -*}
    8.91 +\<close>
    8.92  
    8.93  lemma (in group) one_in_subset:
    8.94    "[| H \<subseteq> carrier G; H \<noteq> {}; \<forall>a \<in> H. inv a \<in> H; \<forall>a\<in>H. \<forall>b\<in>H. a \<otimes> b \<in> H |]
    8.95     ==> \<one> \<in> H"
    8.96  by force
    8.97  
    8.98 -text {* A characterization of subgroups: closed, non-empty subset. *}
    8.99 +text \<open>A characterization of subgroups: closed, non-empty subset.\<close>
   8.100  
   8.101  lemma (in group) subgroupI:
   8.102    assumes subset: "H \<subseteq> carrier G" and non_empty: "H \<noteq> {}"
   8.103 @@ -513,7 +513,7 @@
   8.104  *)
   8.105  
   8.106  
   8.107 -subsection {* Direct Products *}
   8.108 +subsection \<open>Direct Products\<close>
   8.109  
   8.110  definition
   8.111    DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid" (infixr "\<times>\<times>" 80) where
   8.112 @@ -533,7 +533,7 @@
   8.113  qed
   8.114  
   8.115  
   8.116 -text{*Does not use the previous result because it's easier just to use auto.*}
   8.117 +text\<open>Does not use the previous result because it's easier just to use auto.\<close>
   8.118  lemma DirProd_group:
   8.119    assumes "group G" and "group H"
   8.120    shows "group (G \<times>\<times> H)"
   8.121 @@ -571,7 +571,7 @@
   8.122  qed
   8.123  
   8.124  
   8.125 -subsection {* Homomorphisms and Isomorphisms *}
   8.126 +subsection \<open>Homomorphisms and Isomorphisms\<close>
   8.127  
   8.128  definition
   8.129    hom :: "_ => _ => ('a => 'b) set" where
   8.130 @@ -611,8 +611,8 @@
   8.131  by (auto simp add: iso_def hom_def inj_on_def bij_betw_def)
   8.132  
   8.133  
   8.134 -text{*Basis for homomorphism proofs: we assume two groups @{term G} and
   8.135 -  @{term H}, with a homomorphism @{term h} between them*}
   8.136 +text\<open>Basis for homomorphism proofs: we assume two groups @{term G} and
   8.137 +  @{term H}, with a homomorphism @{term h} between them\<close>
   8.138  locale group_hom = G: group G + H: group H for G (structure) and H (structure) +
   8.139    fixes h
   8.140    assumes homh: "h \<in> hom G H"
   8.141 @@ -665,13 +665,13 @@
   8.142    unfolding hom_def by (simp add: int_pow_mult)
   8.143  
   8.144  
   8.145 -subsection {* Commutative Structures *}
   8.146 +subsection \<open>Commutative Structures\<close>
   8.147  
   8.148 -text {*
   8.149 +text \<open>
   8.150    Naming convention: multiplicative structures that are commutative
   8.151    are called \emph{commutative}, additive structures are called
   8.152    \emph{Abelian}.
   8.153 -*}
   8.154 +\<close>
   8.155  
   8.156  locale comm_monoid = monoid +
   8.157    assumes m_comm: "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x \<otimes> y = y \<otimes> x"
   8.158 @@ -753,9 +753,9 @@
   8.159    by (simp add: m_ac inv_mult_group)
   8.160  
   8.161  
   8.162 -subsection {* The Lattice of Subgroups of a Group *}
   8.163 +subsection \<open>The Lattice of Subgroups of a Group\<close>
   8.164  
   8.165 -text_raw {* \label{sec:subgroup-lattice} *}
   8.166 +text_raw \<open>\label{sec:subgroup-lattice}\<close>
   8.167  
   8.168  theorem (in group) subgroups_partial_order:
   8.169    "partial_order \<lparr>carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq>\<rparr>"
     9.1 --- a/src/HOL/Algebra/Ideal.thy	Sat Oct 10 16:21:34 2015 +0200
     9.2 +++ b/src/HOL/Algebra/Ideal.thy	Sat Oct 10 16:26:23 2015 +0200
     9.3 @@ -6,11 +6,11 @@
     9.4  imports Ring AbelCoset
     9.5  begin
     9.6  
     9.7 -section {* Ideals *}
     9.8 +section \<open>Ideals\<close>
     9.9  
    9.10 -subsection {* Definitions *}
    9.11 +subsection \<open>Definitions\<close>
    9.12  
    9.13 -subsubsection {* General definition *}
    9.14 +subsubsection \<open>General definition\<close>
    9.15  
    9.16  locale ideal = additive_subgroup I R + ring R for I and R (structure) +
    9.17    assumes I_l_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
    9.18 @@ -44,12 +44,12 @@
    9.19  qed
    9.20  
    9.21  
    9.22 -subsubsection (in ring) {* Ideals Generated by a Subset of @{term "carrier R"} *}
    9.23 +subsubsection (in ring) \<open>Ideals Generated by a Subset of @{term "carrier R"}\<close>
    9.24  
    9.25  definition genideal :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set"  ("Idl\<index> _" [80] 79)
    9.26    where "genideal R S = Inter {I. ideal I R \<and> S \<subseteq> I}"
    9.27  
    9.28 -subsubsection {* Principal Ideals *}
    9.29 +subsubsection \<open>Principal Ideals\<close>
    9.30  
    9.31  locale principalideal = ideal +
    9.32    assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}"
    9.33 @@ -70,7 +70,7 @@
    9.34  qed
    9.35  
    9.36  
    9.37 -subsubsection {* Maximal Ideals *}
    9.38 +subsubsection \<open>Maximal Ideals\<close>
    9.39  
    9.40  locale maximalideal = ideal +
    9.41    assumes I_notcarr: "carrier R \<noteq> I"
    9.42 @@ -93,7 +93,7 @@
    9.43  qed
    9.44  
    9.45  
    9.46 -subsubsection {* Prime Ideals *}
    9.47 +subsubsection \<open>Prime Ideals\<close>
    9.48  
    9.49  locale primeideal = ideal + cring +
    9.50    assumes I_notcarr: "carrier R \<noteq> I"
    9.51 @@ -140,7 +140,7 @@
    9.52  qed
    9.53  
    9.54  
    9.55 -subsection {* Special Ideals *}
    9.56 +subsection \<open>Special Ideals\<close>
    9.57  
    9.58  lemma (in ring) zeroideal: "ideal {\<zero>} R"
    9.59    apply (intro idealI subgroup.intro)
    9.60 @@ -166,7 +166,7 @@
    9.61  qed
    9.62  
    9.63  
    9.64 -subsection {* General Ideal Properies *}
    9.65 +subsection \<open>General Ideal Properies\<close>
    9.66  
    9.67  lemma (in ideal) one_imp_carrier:
    9.68    assumes I_one_closed: "\<one> \<in> I"
    9.69 @@ -187,10 +187,10 @@
    9.70    using iI by (rule a_Hcarr)
    9.71  
    9.72  
    9.73 -subsection {* Intersection of Ideals *}
    9.74 +subsection \<open>Intersection of Ideals\<close>
    9.75  
    9.76 -text {* \paragraph{Intersection of two ideals} The intersection of any
    9.77 -  two ideals is again an ideal in @{term R} *}
    9.78 +text \<open>\paragraph{Intersection of two ideals} The intersection of any
    9.79 +  two ideals is again an ideal in @{term R}\<close>
    9.80  lemma (in ring) i_intersect:
    9.81    assumes "ideal I R"
    9.82    assumes "ideal J R"
    9.83 @@ -212,8 +212,8 @@
    9.84      done
    9.85  qed
    9.86  
    9.87 -text {* The intersection of any Number of Ideals is again
    9.88 -        an Ideal in @{term R} *}
    9.89 +text \<open>The intersection of any Number of Ideals is again
    9.90 +        an Ideal in @{term R}\<close>
    9.91  lemma (in ring) i_Intersect:
    9.92    assumes Sideals: "\<And>I. I \<in> S \<Longrightarrow> ideal I R"
    9.93      and notempty: "S \<noteq> {}"
    9.94 @@ -291,7 +291,7 @@
    9.95  qed
    9.96  
    9.97  
    9.98 -subsection {* Addition of Ideals *}
    9.99 +subsection \<open>Addition of Ideals\<close>
   9.100  
   9.101  lemma (in ring) add_ideals:
   9.102    assumes idealI: "ideal I R"
   9.103 @@ -335,9 +335,9 @@
   9.104  qed
   9.105  
   9.106  
   9.107 -subsection (in ring) {* Ideals generated by a subset of @{term "carrier R"} *}
   9.108 +subsection (in ring) \<open>Ideals generated by a subset of @{term "carrier R"}\<close>
   9.109  
   9.110 -text {* @{term genideal} generates an ideal *}
   9.111 +text \<open>@{term genideal} generates an ideal\<close>
   9.112  lemma (in ring) genideal_ideal:
   9.113    assumes Scarr: "S \<subseteq> carrier R"
   9.114    shows "ideal (Idl S) R"
   9.115 @@ -360,14 +360,14 @@
   9.116    then show "i \<in> Idl {i}" by fast
   9.117  qed
   9.118  
   9.119 -text {* @{term genideal} generates the minimal ideal *}
   9.120 +text \<open>@{term genideal} generates the minimal ideal\<close>
   9.121  lemma (in ring) genideal_minimal:
   9.122    assumes a: "ideal I R"
   9.123      and b: "S \<subseteq> I"
   9.124    shows "Idl S \<subseteq> I"
   9.125    unfolding genideal_def by rule (elim InterD, simp add: a b)
   9.126  
   9.127 -text {* Generated ideals and subsets *}
   9.128 +text \<open>Generated ideals and subsets\<close>
   9.129  lemma (in ring) Idl_subset_ideal:
   9.130    assumes Iideal: "ideal I R"
   9.131      and Hcarr: "H \<subseteq> carrier R"
   9.132 @@ -425,12 +425,12 @@
   9.133  qed
   9.134  
   9.135  
   9.136 -text {* Generation of Principal Ideals in Commutative Rings *}
   9.137 +text \<open>Generation of Principal Ideals in Commutative Rings\<close>
   9.138  
   9.139  definition cgenideal :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set"  ("PIdl\<index> _" [80] 79)
   9.140    where "cgenideal R a = {x \<otimes>\<^bsub>R\<^esub> a | x. x \<in> carrier R}"
   9.141  
   9.142 -text {* genhideal (?) really generates an ideal *}
   9.143 +text \<open>genhideal (?) really generates an ideal\<close>
   9.144  lemma (in cring) cgenideal_ideal:
   9.145    assumes acarr: "a \<in> carrier R"
   9.146    shows "ideal (PIdl a) R"
   9.147 @@ -499,7 +499,7 @@
   9.148      by fast
   9.149  qed
   9.150  
   9.151 -text {* @{const "cgenideal"} is minimal *}
   9.152 +text \<open>@{const "cgenideal"} is minimal\<close>
   9.153  
   9.154  lemma (in ring) cgenideal_minimal:
   9.155    assumes "ideal J R"
   9.156 @@ -544,7 +544,7 @@
   9.157  qed
   9.158  
   9.159  
   9.160 -subsection {* Union of Ideals *}
   9.161 +subsection \<open>Union of Ideals\<close>
   9.162  
   9.163  lemma (in ring) union_genideal:
   9.164    assumes idealI: "ideal I R"
   9.165 @@ -589,16 +589,16 @@
   9.166  qed
   9.167  
   9.168  
   9.169 -subsection {* Properties of Principal Ideals *}
   9.170 +subsection \<open>Properties of Principal Ideals\<close>
   9.171  
   9.172 -text {* @{text "\<zero>"} generates the zero ideal *}
   9.173 +text \<open>@{text "\<zero>"} generates the zero ideal\<close>
   9.174  lemma (in ring) zero_genideal: "Idl {\<zero>} = {\<zero>}"
   9.175    apply rule
   9.176    apply (simp add: genideal_minimal zeroideal)
   9.177    apply (fast intro!: genideal_self)
   9.178    done
   9.179  
   9.180 -text {* @{text "\<one>"} generates the unit ideal *}
   9.181 +text \<open>@{text "\<one>"} generates the unit ideal\<close>
   9.182  lemma (in ring) one_genideal: "Idl {\<one>} = carrier R"
   9.183  proof -
   9.184    have "\<one> \<in> Idl {\<one>}"
   9.185 @@ -608,14 +608,14 @@
   9.186  qed
   9.187  
   9.188  
   9.189 -text {* The zero ideal is a principal ideal *}
   9.190 +text \<open>The zero ideal is a principal ideal\<close>
   9.191  corollary (in ring) zeropideal: "principalideal {\<zero>} R"
   9.192    apply (rule principalidealI)
   9.193     apply (rule zeroideal)
   9.194    apply (blast intro!: zero_genideal[symmetric])
   9.195    done
   9.196  
   9.197 -text {* The unit ideal is a principal ideal *}
   9.198 +text \<open>The unit ideal is a principal ideal\<close>
   9.199  corollary (in ring) onepideal: "principalideal (carrier R) R"
   9.200    apply (rule principalidealI)
   9.201     apply (rule oneideal)
   9.202 @@ -623,7 +623,7 @@
   9.203    done
   9.204  
   9.205  
   9.206 -text {* Every principal ideal is a right coset of the carrier *}
   9.207 +text \<open>Every principal ideal is a right coset of the carrier\<close>
   9.208  lemma (in principalideal) rcos_generate:
   9.209    assumes "cring R"
   9.210    shows "\<exists>x\<in>I. I = carrier R #> x"
   9.211 @@ -650,7 +650,7 @@
   9.212  qed
   9.213  
   9.214  
   9.215 -subsection {* Prime Ideals *}
   9.216 +subsection \<open>Prime Ideals\<close>
   9.217  
   9.218  lemma (in ideal) primeidealCD:
   9.219    assumes "cring R"
   9.220 @@ -683,7 +683,7 @@
   9.221    then show thesis using primeidealCD [OF R.is_cring notprime] by blast
   9.222  qed
   9.223  
   9.224 -text {* If @{text "{\<zero>}"} is a prime ideal of a commutative ring, the ring is a domain *}
   9.225 +text \<open>If @{text "{\<zero>}"} is a prime ideal of a commutative ring, the ring is a domain\<close>
   9.226  lemma (in cring) zeroprimeideal_domainI:
   9.227    assumes pi: "primeideal {\<zero>} R"
   9.228    shows "domain R"
   9.229 @@ -713,7 +713,7 @@
   9.230    done
   9.231  
   9.232  
   9.233 -subsection {* Maximal Ideals *}
   9.234 +subsection \<open>Maximal Ideals\<close>
   9.235  
   9.236  lemma (in ideal) helper_I_closed:
   9.237    assumes carr: "a \<in> carrier R" "x \<in> carrier R" "y \<in> carrier R"
   9.238 @@ -767,7 +767,7 @@
   9.239    qed
   9.240  qed
   9.241  
   9.242 -text {* In a cring every maximal ideal is prime *}
   9.243 +text \<open>In a cring every maximal ideal is prime\<close>
   9.244  lemma (in cring) maximalideal_is_prime:
   9.245    assumes "maximalideal I R"
   9.246    shows "primeideal I R"
   9.247 @@ -825,7 +825,7 @@
   9.248  qed
   9.249  
   9.250  
   9.251 -subsection {* Derived Theorems *}
   9.252 +subsection \<open>Derived Theorems\<close>
   9.253  
   9.254  --"A non-zero cring that has only the two trivial ideals is a field"
   9.255  lemma (in cring) trivialideals_fieldI:
   9.256 @@ -927,7 +927,7 @@
   9.257    by (fast intro!: trivialideals_fieldI[OF carrnzero] field.all_ideals)
   9.258  
   9.259  
   9.260 -text {* Like zeroprimeideal for domains *}
   9.261 +text \<open>Like zeroprimeideal for domains\<close>
   9.262  lemma (in field) zeromaximalideal: "maximalideal {\<zero>} R"
   9.263    apply (rule maximalidealI)
   9.264      apply (rule zeroideal)
    10.1 --- a/src/HOL/Algebra/IntRing.thy	Sat Oct 10 16:21:34 2015 +0200
    10.2 +++ b/src/HOL/Algebra/IntRing.thy	Sat Oct 10 16:26:23 2015 +0200
    10.3 @@ -7,9 +7,9 @@
    10.4  imports QuotRing Lattice Int "~~/src/HOL/Number_Theory/Primes"
    10.5  begin
    10.6  
    10.7 -section {* The Ring of Integers *}
    10.8 +section \<open>The Ring of Integers\<close>
    10.9  
   10.10 -subsection {* Some properties of @{typ int} *}
   10.11 +subsection \<open>Some properties of @{typ int}\<close>
   10.12  
   10.13  lemma dvds_eq_abseq:
   10.14    fixes k :: int
   10.15 @@ -20,7 +20,7 @@
   10.16  done
   10.17  
   10.18  
   10.19 -subsection {* @{text "\<Z>"}: The Set of Integers as Algebraic Structure *}
   10.20 +subsection \<open>@{text "\<Z>"}: The Set of Integers as Algebraic Structure\<close>
   10.21  
   10.22  abbreviation int_ring :: "int ring" ("\<Z>")
   10.23    where "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
   10.24 @@ -47,11 +47,11 @@
   10.25  *)
   10.26  
   10.27  
   10.28 -subsection {* Interpretations *}
   10.29 +subsection \<open>Interpretations\<close>
   10.30  
   10.31 -text {* Since definitions of derived operations are global, their
   10.32 +text \<open>Since definitions of derived operations are global, their
   10.33    interpretation needs to be done as early as possible --- that is,
   10.34 -  with as few assumptions as possible. *}
   10.35 +  with as few assumptions as possible.\<close>
   10.36  
   10.37  interpretation int: monoid \<Z>
   10.38    where "carrier \<Z> = UNIV"
   10.39 @@ -159,8 +159,8 @@
   10.40  qed (simp add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq int_a_inv_eq int_a_minus_eq)+
   10.41  
   10.42  
   10.43 -text {* Removal of occurrences of @{term UNIV} in interpretation result
   10.44 -  --- experimental. *}
   10.45 +text \<open>Removal of occurrences of @{term UNIV} in interpretation result
   10.46 +  --- experimental.\<close>
   10.47  
   10.48  lemma UNIV:
   10.49    "x \<in> UNIV \<longleftrightarrow> True"
   10.50 @@ -218,7 +218,7 @@
   10.51    by standard clarsimp
   10.52  
   10.53  
   10.54 -subsection {* Generated Ideals of @{text "\<Z>"} *}
   10.55 +subsection \<open>Generated Ideals of @{text "\<Z>"}\<close>
   10.56  
   10.57  lemma int_Idl: "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}"
   10.58    apply (subst int.cgenideal_eq_genideal[symmetric]) apply simp
   10.59 @@ -255,7 +255,7 @@
   10.60  qed
   10.61  
   10.62  
   10.63 -subsection {* Ideals and Divisibility *}
   10.64 +subsection \<open>Ideals and Divisibility\<close>
   10.65  
   10.66  lemma int_Idl_subset_ideal: "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})"
   10.67    by (rule int.Idl_subset_ideal') simp_all
   10.68 @@ -287,7 +287,7 @@
   10.69    done
   10.70  
   10.71  
   10.72 -subsection {* Ideals and the Modulus *}
   10.73 +subsection \<open>Ideals and the Modulus\<close>
   10.74  
   10.75  definition ZMod :: "int \<Rightarrow> int \<Rightarrow> int set"
   10.76    where "ZMod k r = (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
   10.77 @@ -370,7 +370,7 @@
   10.78    done
   10.79  
   10.80  
   10.81 -subsection {* Factorization *}
   10.82 +subsection \<open>Factorization\<close>
   10.83  
   10.84  definition ZFact :: "int \<Rightarrow> int set ring"
   10.85    where "ZFact k = \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
    11.1 --- a/src/HOL/Algebra/Lattice.thy	Sat Oct 10 16:21:34 2015 +0200
    11.2 +++ b/src/HOL/Algebra/Lattice.thy	Sat Oct 10 16:26:23 2015 +0200
    11.3 @@ -9,9 +9,9 @@
    11.4  imports Congruence
    11.5  begin
    11.6  
    11.7 -section {* Orders and Lattices *}
    11.8 +section \<open>Orders and Lattices\<close>
    11.9  
   11.10 -subsection {* Partial Orders *}
   11.11 +subsection \<open>Partial Orders\<close>
   11.12  
   11.13  record 'a gorder = "'a eq_object" +
   11.14    le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
   11.15 @@ -32,7 +32,7 @@
   11.16    where "x \<sqsubset>\<^bsub>L\<^esub> y \<longleftrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> y & x .\<noteq>\<^bsub>L\<^esub> y"
   11.17  
   11.18  
   11.19 -subsubsection {* The order relation *}
   11.20 +subsubsection \<open>The order relation\<close>
   11.21  
   11.22  context weak_partial_order
   11.23  begin
   11.24 @@ -103,7 +103,7 @@
   11.25    using assms unfolding lless_def by (blast dest: le_trans intro: sym)
   11.26  
   11.27  
   11.28 -subsubsection {* Upper and lower bounds of a set *}
   11.29 +subsubsection \<open>Upper and lower bounds of a set\<close>
   11.30  
   11.31  definition
   11.32    Upper :: "[_, 'a set] => 'a set"
   11.33 @@ -276,7 +276,7 @@
   11.34  qed
   11.35  
   11.36  
   11.37 -subsubsection {* Least and greatest, as predicate *}
   11.38 +subsubsection \<open>Least and greatest, as predicate\<close>
   11.39  
   11.40  definition
   11.41    least :: "[_, 'a, 'a set] => bool"
   11.42 @@ -286,8 +286,8 @@
   11.43    greatest :: "[_, 'a, 'a set] => bool"
   11.44    where "greatest L g A \<longleftrightarrow> A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq>\<^bsub>L\<^esub> g)"
   11.45  
   11.46 -text (in weak_partial_order) {* Could weaken these to @{term "l \<in> carrier L \<and> l
   11.47 -  .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}. *}
   11.48 +text (in weak_partial_order) \<open>Could weaken these to @{term "l \<in> carrier L \<and> l
   11.49 +  .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}.\<close>
   11.50  
   11.51  lemma least_closed [intro, simp]:
   11.52    "least L l A ==> l \<in> carrier L"
   11.53 @@ -310,8 +310,8 @@
   11.54    "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> least L x A = least L x' A"
   11.55    by (unfold least_def) (auto dest: sym)
   11.56  
   11.57 -text (in weak_partial_order) {* @{const least} is not congruent in the second parameter for 
   11.58 -  @{term "A {.=} A'"} *}
   11.59 +text (in weak_partial_order) \<open>@{const least} is not congruent in the second parameter for 
   11.60 +  @{term "A {.=} A'"}\<close>
   11.61  
   11.62  lemma (in weak_partial_order) least_Upper_cong_l:
   11.63    assumes "x .= x'"
   11.64 @@ -367,8 +367,8 @@
   11.65    greatest L x A = greatest L x' A"
   11.66    by (unfold greatest_def) (auto dest: sym)
   11.67  
   11.68 -text (in weak_partial_order) {* @{const greatest} is not congruent in the second parameter for 
   11.69 -  @{term "A {.=} A'"} *}
   11.70 +text (in weak_partial_order) \<open>@{const greatest} is not congruent in the second parameter for 
   11.71 +  @{term "A {.=} A'"}\<close>
   11.72  
   11.73  lemma (in weak_partial_order) greatest_Lower_cong_l:
   11.74    assumes "x .= x'"
   11.75 @@ -402,7 +402,7 @@
   11.76    shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
   11.77    by (unfold greatest_def) blast
   11.78  
   11.79 -text {* Supremum and infimum *}
   11.80 +text \<open>Supremum and infimum\<close>
   11.81  
   11.82  definition
   11.83    sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
   11.84 @@ -421,7 +421,7 @@
   11.85    where "x \<sqinter>\<^bsub>L\<^esub> y = \<Sqinter>\<^bsub>L\<^esub>{x, y}"
   11.86  
   11.87  
   11.88 -subsection {* Lattices *}
   11.89 +subsection \<open>Lattices\<close>
   11.90  
   11.91  locale weak_upper_semilattice = weak_partial_order +
   11.92    assumes sup_of_two_exists:
   11.93 @@ -434,7 +434,7 @@
   11.94  locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice
   11.95  
   11.96  
   11.97 -subsubsection {* Supremum *}
   11.98 +subsubsection \<open>Supremum\<close>
   11.99  
  11.100  lemma (in weak_upper_semilattice) joinI:
  11.101    "[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |]
  11.102 @@ -507,7 +507,7 @@
  11.103    unfolding sup_def
  11.104    by (rule someI2) (auto intro: sup_of_singletonI)
  11.105  
  11.106 -text {* Condition on @{text A}: supremum exists. *}
  11.107 +text \<open>Condition on @{text A}: supremum exists.\<close>
  11.108  
  11.109  lemma (in weak_upper_semilattice) sup_insertI:
  11.110    "[| !!s. least L s (Upper L (insert x A)) ==> P s;
  11.111 @@ -638,7 +638,7 @@
  11.112    assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
  11.113    shows "x \<squnion> (y \<squnion> z) .= \<Squnion>{x, y, z}"
  11.114  proof (rule finite_sup_insertI)
  11.115 -  -- {* The textbook argument in Jacobson I, p 457 *}
  11.116 +  -- \<open>The textbook argument in Jacobson I, p 457\<close>
  11.117    fix s
  11.118    assume sup: "least L s (Upper L {x, y, z})"
  11.119    show "x \<squnion> (y \<squnion> z) .= s"
  11.120 @@ -652,7 +652,7 @@
  11.121    qed (simp_all add: L least_closed [OF sup])
  11.122  qed (simp_all add: L)
  11.123  
  11.124 -text {* Commutativity holds for @{text "="}. *}
  11.125 +text \<open>Commutativity holds for @{text "="}.\<close>
  11.126  
  11.127  lemma join_comm:
  11.128    fixes L (structure)
  11.129 @@ -673,7 +673,7 @@
  11.130  qed
  11.131  
  11.132  
  11.133 -subsubsection {* Infimum *}
  11.134 +subsubsection \<open>Infimum\<close>
  11.135  
  11.136  lemma (in weak_lower_semilattice) meetI:
  11.137    "[| !!i. greatest L i (Lower L {x, y}) ==> P i;
  11.138 @@ -747,7 +747,7 @@
  11.139    unfolding inf_def
  11.140    by (rule someI2) (auto intro: inf_of_singletonI)
  11.141  
  11.142 -text {* Condition on @{text A}: infimum exists. *}
  11.143 +text \<open>Condition on @{text A}: infimum exists.\<close>
  11.144  
  11.145  lemma (in weak_lower_semilattice) inf_insertI:
  11.146    "[| !!i. greatest L i (Lower L (insert x A)) ==> P i;
  11.147 @@ -879,7 +879,7 @@
  11.148    assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
  11.149    shows "x \<sqinter> (y \<sqinter> z) .= \<Sqinter>{x, y, z}"
  11.150  proof (rule finite_inf_insertI)
  11.151 -  txt {* The textbook argument in Jacobson I, p 457 *}
  11.152 +  txt \<open>The textbook argument in Jacobson I, p 457\<close>
  11.153    fix i
  11.154    assume inf: "greatest L i (Lower L {x, y, z})"
  11.155    show "x \<sqinter> (y \<sqinter> z) .= i"
  11.156 @@ -911,19 +911,19 @@
  11.157  qed
  11.158  
  11.159  
  11.160 -subsection {* Total Orders *}
  11.161 +subsection \<open>Total Orders\<close>
  11.162  
  11.163  locale weak_total_order = weak_partial_order +
  11.164    assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
  11.165  
  11.166 -text {* Introduction rule: the usual definition of total order *}
  11.167 +text \<open>Introduction rule: the usual definition of total order\<close>
  11.168  
  11.169  lemma (in weak_partial_order) weak_total_orderI:
  11.170    assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
  11.171    shows "weak_total_order L"
  11.172    by standard (rule total)
  11.173  
  11.174 -text {* Total orders are lattices. *}
  11.175 +text \<open>Total orders are lattices.\<close>
  11.176  
  11.177  sublocale weak_total_order < weak: weak_lattice
  11.178  proof
  11.179 @@ -969,7 +969,7 @@
  11.180  qed
  11.181  
  11.182  
  11.183 -subsection {* Complete Lattices *}
  11.184 +subsection \<open>Complete Lattices\<close>
  11.185  
  11.186  locale weak_complete_lattice = weak_lattice +
  11.187    assumes sup_exists:
  11.188 @@ -977,7 +977,7 @@
  11.189      and inf_exists:
  11.190      "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
  11.191  
  11.192 -text {* Introduction rule: the usual definition of complete lattice *}
  11.193 +text \<open>Introduction rule: the usual definition of complete lattice\<close>
  11.194  
  11.195  lemma (in weak_partial_order) weak_complete_latticeI:
  11.196    assumes sup_exists:
  11.197 @@ -1034,7 +1034,7 @@
  11.198    "\<bottom> \<in> carrier L"
  11.199    by (unfold bottom_def) simp
  11.200  
  11.201 -text {* Jacobson: Theorem 8.1 *}
  11.202 +text \<open>Jacobson: Theorem 8.1\<close>
  11.203  
  11.204  lemma Lower_empty [simp]:
  11.205    "Lower L {} = carrier L"
  11.206 @@ -1090,7 +1090,7 @@
  11.207  (* TODO: prove dual version *)
  11.208  
  11.209  
  11.210 -subsection {* Orders and Lattices where @{text eq} is the Equality *}
  11.211 +subsection \<open>Orders and Lattices where @{text eq} is the Equality\<close>
  11.212  
  11.213  locale partial_order = weak_partial_order +
  11.214    assumes eq_is_equal: "op .= = op ="
  11.215 @@ -1115,7 +1115,7 @@
  11.216  end
  11.217  
  11.218  
  11.219 -text {* Least and greatest, as predicate *}
  11.220 +text \<open>Least and greatest, as predicate\<close>
  11.221  
  11.222  lemma (in partial_order) least_unique:
  11.223    "[| least L x A; least L y A |] ==> x = y"
  11.224 @@ -1126,7 +1126,7 @@
  11.225    using weak_greatest_unique unfolding eq_is_equal .
  11.226  
  11.227  
  11.228 -text {* Lattices *}
  11.229 +text \<open>Lattices\<close>
  11.230  
  11.231  locale upper_semilattice = partial_order +
  11.232    assumes sup_of_two_exists:
  11.233 @@ -1145,7 +1145,7 @@
  11.234  locale lattice = upper_semilattice + lower_semilattice
  11.235  
  11.236  
  11.237 -text {* Supremum *}
  11.238 +text \<open>Supremum\<close>
  11.239  
  11.240  declare (in partial_order) weak_sup_of_singleton [simp del]
  11.241  
  11.242 @@ -1164,7 +1164,7 @@
  11.243    using weak_join_assoc L unfolding eq_is_equal .
  11.244  
  11.245  
  11.246 -text {* Infimum *}
  11.247 +text \<open>Infimum\<close>
  11.248  
  11.249  declare (in partial_order) weak_inf_of_singleton [simp del]
  11.250  
  11.251 @@ -1172,7 +1172,7 @@
  11.252    "x \<in> carrier L ==> \<Sqinter>{x} = x"
  11.253    using weak_inf_of_singleton unfolding eq_is_equal .
  11.254  
  11.255 -text {* Condition on @{text A}: infimum exists. *}
  11.256 +text \<open>Condition on @{text A}: infimum exists.\<close>
  11.257  
  11.258  lemma (in lower_semilattice) meet_assoc_lemma:
  11.259    assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
  11.260 @@ -1185,7 +1185,7 @@
  11.261    using weak_meet_assoc L unfolding eq_is_equal .
  11.262  
  11.263  
  11.264 -text {* Total Orders *}
  11.265 +text \<open>Total Orders\<close>
  11.266  
  11.267  locale total_order = partial_order +
  11.268    assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
  11.269 @@ -1193,20 +1193,20 @@
  11.270  sublocale total_order < weak: weak_total_order
  11.271    by standard (rule total_order_total)
  11.272  
  11.273 -text {* Introduction rule: the usual definition of total order *}
  11.274 +text \<open>Introduction rule: the usual definition of total order\<close>
  11.275  
  11.276  lemma (in partial_order) total_orderI:
  11.277    assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
  11.278    shows "total_order L"
  11.279    by standard (rule total)
  11.280  
  11.281 -text {* Total orders are lattices. *}
  11.282 +text \<open>Total orders are lattices.\<close>
  11.283  
  11.284  sublocale total_order < weak: lattice
  11.285    by standard (auto intro: sup_of_two_exists inf_of_two_exists)
  11.286  
  11.287  
  11.288 -text {* Complete lattices *}
  11.289 +text \<open>Complete lattices\<close>
  11.290  
  11.291  locale complete_lattice = lattice +
  11.292    assumes sup_exists:
  11.293 @@ -1217,7 +1217,7 @@
  11.294  sublocale complete_lattice < weak: weak_complete_lattice
  11.295    by standard (auto intro: sup_exists inf_exists)
  11.296  
  11.297 -text {* Introduction rule: the usual definition of complete lattice *}
  11.298 +text \<open>Introduction rule: the usual definition of complete lattice\<close>
  11.299  
  11.300  lemma (in partial_order) complete_latticeI:
  11.301    assumes sup_exists:
  11.302 @@ -1273,9 +1273,9 @@
  11.303  (* TODO: prove dual version *)
  11.304  
  11.305  
  11.306 -subsection {* Examples *}
  11.307 +subsection \<open>Examples\<close>
  11.308  
  11.309 -subsubsection {* The Powerset of a Set is a Complete Lattice *}
  11.310 +subsubsection \<open>The Powerset of a Set is a Complete Lattice\<close>
  11.311  
  11.312  theorem powerset_is_complete_lattice:
  11.313    "complete_lattice \<lparr>carrier = Pow A, eq = op =, le = op \<subseteq>\<rparr>"
  11.314 @@ -1293,13 +1293,13 @@
  11.315    fix B
  11.316    assume "B \<subseteq> carrier ?L"
  11.317    then have "greatest ?L (\<Inter>B \<inter> A) (Lower ?L B)"
  11.318 -    txt {* @{term "\<Inter>B"} is not the infimum of @{term B}:
  11.319 -      @{term "\<Inter>{} = UNIV"} which is in general bigger than @{term "A"}! *}
  11.320 +    txt \<open>@{term "\<Inter>B"} is not the infimum of @{term B}:
  11.321 +      @{term "\<Inter>{} = UNIV"} which is in general bigger than @{term "A"}!\<close>
  11.322      by (fastforce intro!: greatest_LowerI simp: Lower_def)
  11.323    then show "EX i. greatest ?L i (Lower ?L B)" ..
  11.324  qed
  11.325  
  11.326 -text {* An other example, that of the lattice of subgroups of a group,
  11.327 -  can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *}
  11.328 +text \<open>An other example, that of the lattice of subgroups of a group,
  11.329 +  can be found in Group theory (Section~\ref{sec:subgroup-lattice}).\<close>
  11.330  
  11.331  end
    12.1 --- a/src/HOL/Algebra/Module.thy	Sat Oct 10 16:21:34 2015 +0200
    12.2 +++ b/src/HOL/Algebra/Module.thy	Sat Oct 10 16:26:23 2015 +0200
    12.3 @@ -7,9 +7,9 @@
    12.4  imports Ring
    12.5  begin
    12.6  
    12.7 -section {* Modules over an Abelian Group *}
    12.8 +section \<open>Modules over an Abelian Group\<close>
    12.9  
   12.10 -subsection {* Definitions *}
   12.11 +subsection \<open>Definitions\<close>
   12.12  
   12.13  record ('a, 'b) module = "'b ring" +
   12.14    smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)
   12.15 @@ -103,7 +103,7 @@
   12.16      smult_l_distr smult_r_distr smult_assoc1)
   12.17  
   12.18  
   12.19 -subsection {* Basic Properties of Algebras *}
   12.20 +subsection \<open>Basic Properties of Algebras\<close>
   12.21  
   12.22  lemma (in algebra) smult_l_null [simp]:
   12.23    "x \<in> carrier M ==> \<zero> \<odot>\<^bsub>M\<^esub> x = \<zero>\<^bsub>M\<^esub>"
    13.1 --- a/src/HOL/Algebra/QuotRing.thy	Sat Oct 10 16:21:34 2015 +0200
    13.2 +++ b/src/HOL/Algebra/QuotRing.thy	Sat Oct 10 16:26:23 2015 +0200
    13.3 @@ -6,17 +6,17 @@
    13.4  imports RingHom
    13.5  begin
    13.6  
    13.7 -section {* Quotient Rings *}
    13.8 +section \<open>Quotient Rings\<close>
    13.9  
   13.10 -subsection {* Multiplication on Cosets *}
   13.11 +subsection \<open>Multiplication on Cosets\<close>
   13.12  
   13.13  definition rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set"
   13.14      ("[mod _:] _ \<Otimes>\<index> _" [81,81,81] 80)
   13.15    where "rcoset_mult R I A B = (\<Union>a\<in>A. \<Union>b\<in>B. I +>\<^bsub>R\<^esub> (a \<otimes>\<^bsub>R\<^esub> b))"
   13.16  
   13.17  
   13.18 -text {* @{const "rcoset_mult"} fulfils the properties required by
   13.19 -  congruences *}
   13.20 +text \<open>@{const "rcoset_mult"} fulfils the properties required by
   13.21 +  congruences\<close>
   13.22  lemma (in ideal) rcoset_mult_add:
   13.23      "x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> [mod I:] (I +> x) \<Otimes> (I +> y) = I +> (x \<otimes> y)"
   13.24    apply rule
   13.25 @@ -70,7 +70,7 @@
   13.26  qed
   13.27  
   13.28  
   13.29 -subsection {* Quotient Ring Definition *}
   13.30 +subsection \<open>Quotient Ring Definition\<close>
   13.31  
   13.32  definition FactRing :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) ring"
   13.33      (infixl "Quot" 65)
   13.34 @@ -79,33 +79,33 @@
   13.35        one = (I +>\<^bsub>R\<^esub> \<one>\<^bsub>R\<^esub>), zero = I, add = set_add R\<rparr>"
   13.36  
   13.37  
   13.38 -subsection {* Factorization over General Ideals *}
   13.39 +subsection \<open>Factorization over General Ideals\<close>
   13.40  
   13.41 -text {* The quotient is a ring *}
   13.42 +text \<open>The quotient is a ring\<close>
   13.43  lemma (in ideal) quotient_is_ring: "ring (R Quot I)"
   13.44  apply (rule ringI)
   13.45 -   --{* abelian group *}
   13.46 +   --\<open>abelian group\<close>
   13.47     apply (rule comm_group_abelian_groupI)
   13.48     apply (simp add: FactRing_def)
   13.49     apply (rule a_factorgroup_is_comm_group[unfolded A_FactGroup_def'])
   13.50 -  --{* mult monoid *}
   13.51 +  --\<open>mult monoid\<close>
   13.52    apply (rule monoidI)
   13.53        apply (simp_all add: FactRing_def A_RCOSETS_def RCOSETS_def
   13.54               a_r_coset_def[symmetric])
   13.55 -      --{* mult closed *}
   13.56 +      --\<open>mult closed\<close>
   13.57        apply (clarify)
   13.58        apply (simp add: rcoset_mult_add, fast)
   13.59 -     --{* mult @{text one_closed} *}
   13.60 +     --\<open>mult @{text one_closed}\<close>
   13.61       apply force
   13.62 -    --{* mult assoc *}
   13.63 +    --\<open>mult assoc\<close>
   13.64      apply clarify
   13.65      apply (simp add: rcoset_mult_add m_assoc)
   13.66 -   --{* mult one *}
   13.67 +   --\<open>mult one\<close>
   13.68     apply clarify
   13.69     apply (simp add: rcoset_mult_add)
   13.70    apply clarify
   13.71    apply (simp add: rcoset_mult_add)
   13.72 - --{* distr *}
   13.73 + --\<open>distr\<close>
   13.74   apply clarify
   13.75   apply (simp add: rcoset_mult_add a_rcos_sum l_distr)
   13.76  apply clarify
   13.77 @@ -113,7 +113,7 @@
   13.78  done
   13.79  
   13.80  
   13.81 -text {* This is a ring homomorphism *}
   13.82 +text \<open>This is a ring homomorphism\<close>
   13.83  
   13.84  lemma (in ideal) rcos_ring_hom: "(op +> I) \<in> ring_hom R (R Quot I)"
   13.85  apply (rule ring_hom_memI)
   13.86 @@ -132,7 +132,7 @@
   13.87  apply (simp add: FactRing_def)
   13.88  done
   13.89  
   13.90 -text {* The quotient of a cring is also commutative *}
   13.91 +text \<open>The quotient of a cring is also commutative\<close>
   13.92  lemma (in ideal) quotient_is_cring:
   13.93    assumes "cring R"
   13.94    shows "cring (R Quot I)"
   13.95 @@ -148,7 +148,7 @@
   13.96      done
   13.97  qed
   13.98  
   13.99 -text {* Cosets as a ring homomorphism on crings *}
  13.100 +text \<open>Cosets as a ring homomorphism on crings\<close>
  13.101  lemma (in ideal) rcos_ring_hom_cring:
  13.102    assumes "cring R"
  13.103    shows "ring_hom_cring R (R Quot I) (op +> I)"
  13.104 @@ -164,9 +164,9 @@
  13.105  qed
  13.106  
  13.107  
  13.108 -subsection {* Factorization over Prime Ideals *}
  13.109 +subsection \<open>Factorization over Prime Ideals\<close>
  13.110  
  13.111 -text {* The quotient ring generated by a prime ideal is a domain *}
  13.112 +text \<open>The quotient ring generated by a prime ideal is a domain\<close>
  13.113  lemma (in primeideal) quotient_is_domain: "domain (R Quot I)"
  13.114    apply (rule domain.intro)
  13.115     apply (rule quotient_is_cring, rule is_cring)
  13.116 @@ -201,18 +201,18 @@
  13.117    then show "I +> x = I" by (rule a_rcos_const)
  13.118  qed
  13.119  
  13.120 -text {* Generating right cosets of a prime ideal is a homomorphism
  13.121 -        on commutative rings *}
  13.122 +text \<open>Generating right cosets of a prime ideal is a homomorphism
  13.123 +        on commutative rings\<close>
  13.124  lemma (in primeideal) rcos_ring_hom_cring: "ring_hom_cring R (R Quot I) (op +> I)"
  13.125    by (rule rcos_ring_hom_cring) (rule is_cring)
  13.126  
  13.127  
  13.128 -subsection {* Factorization over Maximal Ideals *}
  13.129 +subsection \<open>Factorization over Maximal Ideals\<close>
  13.130  
  13.131 -text {* In a commutative ring, the quotient ring over a maximal ideal
  13.132 +text \<open>In a commutative ring, the quotient ring over a maximal ideal
  13.133          is a field.
  13.134          The proof follows ``W. Adkins, S. Weintraub: Algebra --
  13.135 -        An Approach via Module Theory'' *}
  13.136 +        An Approach via Module Theory''\<close>
  13.137  lemma (in maximalideal) quotient_is_field:
  13.138    assumes "cring R"
  13.139    shows "field (R Quot I)"
  13.140 @@ -225,7 +225,7 @@
  13.141       apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarsimp)
  13.142       apply (simp add: rcoset_mult_add) defer 1
  13.143    proof (rule ccontr, simp)
  13.144 -    --{* Quotient is not empty *}
  13.145 +    --\<open>Quotient is not empty\<close>
  13.146      assume "\<zero>\<^bsub>R Quot I\<^esub> = \<one>\<^bsub>R Quot I\<^esub>"
  13.147      then have II1: "I = I +> \<one>" by (simp add: FactRing_def)
  13.148      from a_rcos_self[OF one_closed] have "\<one> \<in> I"
  13.149 @@ -233,11 +233,11 @@
  13.150      then have "I = carrier R" by (rule one_imp_carrier)
  13.151      with I_notcarr show False by simp
  13.152    next
  13.153 -    --{* Existence of Inverse *}
  13.154 +    --\<open>Existence of Inverse\<close>
  13.155      fix a
  13.156      assume IanI: "I +> a \<noteq> I" and acarr: "a \<in> carrier R"
  13.157  
  13.158 -    --{* Helper ideal @{text "J"} *}
  13.159 +    --\<open>Helper ideal @{text "J"}\<close>
  13.160      def J \<equiv> "(carrier R #> a) <+> I :: 'a set"
  13.161      have idealJ: "ideal J R"
  13.162        apply (unfold J_def, rule add_ideals)
  13.163 @@ -245,7 +245,7 @@
  13.164        apply (rule is_ideal)
  13.165        done
  13.166  
  13.167 -    --{* Showing @{term "J"} not smaller than @{term "I"} *}
  13.168 +    --\<open>Showing @{term "J"} not smaller than @{term "I"}\<close>
  13.169      have IinJ: "I \<subseteq> J"
  13.170      proof (rule, simp add: J_def r_coset_def set_add_defs)
  13.171        fix x
  13.172 @@ -256,7 +256,7 @@
  13.173        with Zcarr and xI show "\<exists>xa\<in>carrier R. \<exists>k\<in>I. x = xa \<otimes> a \<oplus> k" by fast
  13.174      qed
  13.175  
  13.176 -    --{* Showing @{term "J \<noteq> I"} *}
  13.177 +    --\<open>Showing @{term "J \<noteq> I"}\<close>
  13.178      have anI: "a \<notin> I"
  13.179      proof (rule ccontr, simp)
  13.180        assume "a \<in> I"
  13.181 @@ -274,7 +274,7 @@
  13.182  
  13.183      from aJ and anI have JnI: "J \<noteq> I" by fast
  13.184  
  13.185 -    --{* Deducing @{term "J = carrier R"} because @{term "I"} is maximal *}
  13.186 +    --\<open>Deducing @{term "J = carrier R"} because @{term "I"} is maximal\<close>
  13.187      from idealJ and IinJ have "J = I \<or> J = carrier R"
  13.188      proof (rule I_maximal, unfold J_def)
  13.189        have "carrier R #> a \<subseteq> carrier R"
  13.190 @@ -285,7 +285,7 @@
  13.191  
  13.192      with JnI have Jcarr: "J = carrier R" by simp
  13.193  
  13.194 -    --{* Calculating an inverse for @{term "a"} *}
  13.195 +    --\<open>Calculating an inverse for @{term "a"}\<close>
  13.196      from one_closed[folded Jcarr]
  13.197      have "\<exists>r\<in>carrier R. \<exists>i\<in>I. \<one> = r \<otimes> a \<oplus> i"
  13.198        by (simp add: J_def r_coset_def set_add_defs)
  13.199 @@ -294,7 +294,7 @@
  13.200      from one and rcarr and acarr and iI[THEN a_Hcarr]
  13.201      have rai1: "a \<otimes> r = \<ominus>i \<oplus> \<one>" by algebra
  13.202  
  13.203 -    --{* Lifting to cosets *}
  13.204 +    --\<open>Lifting to cosets\<close>
  13.205      from iI have "\<ominus>i \<oplus> \<one> \<in> I +> \<one>"
  13.206        by (intro a_rcosI, simp, intro a_subset, simp)
  13.207      with rai1 have "a \<otimes> r \<in> I +> \<one>" by simp
    14.1 --- a/src/HOL/Algebra/Ring.thy	Sat Oct 10 16:21:34 2015 +0200
    14.2 +++ b/src/HOL/Algebra/Ring.thy	Sat Oct 10 16:26:23 2015 +0200
    14.3 @@ -7,15 +7,15 @@
    14.4  imports FiniteProduct
    14.5  begin
    14.6  
    14.7 -section {* The Algebraic Hierarchy of Rings *}
    14.8 +section \<open>The Algebraic Hierarchy of Rings\<close>
    14.9  
   14.10 -subsection {* Abelian Groups *}
   14.11 +subsection \<open>Abelian Groups\<close>
   14.12  
   14.13  record 'a ring = "'a monoid" +
   14.14    zero :: 'a ("\<zero>\<index>")
   14.15    add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65)
   14.16  
   14.17 -text {* Derived operations. *}
   14.18 +text \<open>Derived operations.\<close>
   14.19  
   14.20  definition
   14.21    a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
   14.22 @@ -39,7 +39,7 @@
   14.23        ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
   14.24  translations
   14.25    "\<Oplus>\<index>i\<in>A. b" \<rightleftharpoons> "CONST finsum \<struct>\<index> (%i. b) A"
   14.26 -  -- {* Beware of argument permutation! *}
   14.27 +  -- \<open>Beware of argument permutation!\<close>
   14.28  
   14.29  
   14.30  locale abelian_group = abelian_monoid +
   14.31 @@ -47,7 +47,7 @@
   14.32       "comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   14.33  
   14.34  
   14.35 -subsection {* Basic Properties *}
   14.36 +subsection \<open>Basic Properties\<close>
   14.37  
   14.38  lemma abelian_monoidI:
   14.39    fixes R (structure)
   14.40 @@ -91,7 +91,7 @@
   14.41  
   14.42  lemmas monoid_record_simps = partial_object.simps monoid.simps
   14.43  
   14.44 -text {* Transfer facts from multiplicative structures via interpretation. *}
   14.45 +text \<open>Transfer facts from multiplicative structures via interpretation.\<close>
   14.46  
   14.47  sublocale abelian_monoid <
   14.48    add!: monoid "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   14.49 @@ -140,9 +140,9 @@
   14.50  lemmas finsum_infinite = add.finprod_infinite
   14.51  
   14.52  lemmas finsum_cong = add.finprod_cong
   14.53 -text {*Usually, if this rule causes a failed congruence proof error,
   14.54 +text \<open>Usually, if this rule causes a failed congruence proof error,
   14.55     the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
   14.56 -   Adding @{thm [source] Pi_def} to the simpset is often useful. *}
   14.57 +   Adding @{thm [source] Pi_def} to the simpset is often useful.\<close>
   14.58  
   14.59  lemmas finsum_reindex = add.finprod_reindex
   14.60  
   14.61 @@ -206,7 +206,7 @@
   14.62  
   14.63  lemmas (in abelian_group) minus_add = add.inv_mult
   14.64   
   14.65 -text {* Derive an @{text "abelian_group"} from a @{text "comm_group"} *}
   14.66 +text \<open>Derive an @{text "abelian_group"} from a @{text "comm_group"}\<close>
   14.67  
   14.68  lemma comm_group_abelian_groupI:
   14.69    fixes G (structure)
   14.70 @@ -219,7 +219,7 @@
   14.71  qed
   14.72  
   14.73  
   14.74 -subsection {* Rings: Basic Definitions *}
   14.75 +subsection \<open>Rings: Basic Definitions\<close>
   14.76  
   14.77  locale semiring = abelian_monoid R + monoid R for R (structure) +
   14.78    assumes l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
   14.79 @@ -246,7 +246,7 @@
   14.80    assumes field_Units: "Units R = carrier R - {\<zero>}"
   14.81  
   14.82  
   14.83 -subsection {* Rings *}
   14.84 +subsection \<open>Rings\<close>
   14.85  
   14.86  lemma ringI:
   14.87    fixes R (structure)
   14.88 @@ -283,8 +283,8 @@
   14.89    shows "cring R"
   14.90  proof (intro cring.intro ring.intro)
   14.91    show "ring_axioms R"
   14.92 -    -- {* Right-distributivity follows from left-distributivity and
   14.93 -          commutativity. *}
   14.94 +    -- \<open>Right-distributivity follows from left-distributivity and
   14.95 +          commutativity.\<close>
   14.96    proof (rule ring_axioms.intro)
   14.97      fix x y z
   14.98      assume R: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
   14.99 @@ -312,7 +312,7 @@
  14.100    "cring R" by (rule cring_axioms)
  14.101  
  14.102  
  14.103 -subsubsection {* Normaliser for Rings *}
  14.104 +subsubsection \<open>Normaliser for Rings\<close>
  14.105  
  14.106  lemma (in abelian_group) r_neg2:
  14.107    "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus> (\<ominus> x \<oplus> y) = y"
  14.108 @@ -335,9 +335,9 @@
  14.109  
  14.110  context ring begin
  14.111  
  14.112 -text {* 
  14.113 +text \<open>
  14.114    The following proofs are from Jacobson, Basic Algebra I, pp.~88--89.
  14.115 -*}
  14.116 +\<close>
  14.117  
  14.118  sublocale semiring
  14.119  proof -
  14.120 @@ -387,20 +387,20 @@
  14.121    "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<ominus> y = x \<oplus> \<ominus> y"
  14.122    by (simp only: a_minus_def)
  14.123  
  14.124 -text {* Setup algebra method:
  14.125 -  compute distributive normal form in locale contexts *}
  14.126 +text \<open>Setup algebra method:
  14.127 +  compute distributive normal form in locale contexts\<close>
  14.128  
  14.129  ML_file "ringsimp.ML"
  14.130  
  14.131 -attribute_setup algebra = {*
  14.132 +attribute_setup algebra = \<open>
  14.133    Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon || Scan.succeed true)
  14.134      -- Scan.lift Args.name -- Scan.repeat Args.term
  14.135      >> (fn ((b, n), ts) => if b then Ringsimp.add_struct (n, ts) else Ringsimp.del_struct (n, ts))
  14.136 -*} "theorems controlling algebra method"
  14.137 +\<close> "theorems controlling algebra method"
  14.138  
  14.139 -method_setup algebra = {*
  14.140 +method_setup algebra = \<open>
  14.141    Scan.succeed (SIMPLE_METHOD' o Ringsimp.algebra_tac)
  14.142 -*} "normalisation of algebraic structure"
  14.143 +\<close> "normalisation of algebraic structure"
  14.144  
  14.145  lemmas (in semiring) semiring_simprules
  14.146    [algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
  14.147 @@ -463,7 +463,7 @@
  14.148  
  14.149  end
  14.150  
  14.151 -text {* Two examples for use of method algebra *}
  14.152 +text \<open>Two examples for use of method algebra\<close>
  14.153  
  14.154  lemma
  14.155    fixes R (structure) and S (structure)
  14.156 @@ -487,7 +487,7 @@
  14.157  qed
  14.158  
  14.159  
  14.160 -subsubsection {* Sums over Finite Sets *}
  14.161 +subsubsection \<open>Sums over Finite Sets\<close>
  14.162  
  14.163  lemma (in semiring) finsum_ldistr:
  14.164    "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
  14.165 @@ -508,7 +508,7 @@
  14.166  qed
  14.167  
  14.168  
  14.169 -subsection {* Integral Domains *}
  14.170 +subsection \<open>Integral Domains\<close>
  14.171  
  14.172  context "domain" begin
  14.173  
  14.174 @@ -554,10 +554,10 @@
  14.175  end
  14.176  
  14.177  
  14.178 -subsection {* Fields *}
  14.179 +subsection \<open>Fields\<close>
  14.180  
  14.181 -text {* Field would not need to be derived from domain, the properties
  14.182 -  for domain follow from the assumptions of field *}
  14.183 +text \<open>Field would not need to be derived from domain, the properties
  14.184 +  for domain follow from the assumptions of field\<close>
  14.185  lemma (in cring) cring_fieldI:
  14.186    assumes field_Units: "Units R = carrier R - {\<zero>}"
  14.187    shows "field R"
  14.188 @@ -585,7 +585,7 @@
  14.189    qed
  14.190  qed (rule field_Units)
  14.191  
  14.192 -text {* Another variant to show that something is a field *}
  14.193 +text \<open>Another variant to show that something is a field\<close>
  14.194  lemma (in cring) cring_fieldI2:
  14.195    assumes notzero: "\<zero> \<noteq> \<one>"
  14.196    and invex: "\<And>a. \<lbrakk>a \<in> carrier R; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>b\<in>carrier R. a \<otimes> b = \<one>"
  14.197 @@ -604,7 +604,7 @@
  14.198  qed
  14.199  
  14.200  
  14.201 -subsection {* Morphisms *}
  14.202 +subsection \<open>Morphisms\<close>
  14.203  
  14.204  definition
  14.205    ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set"
    15.1 --- a/src/HOL/Algebra/RingHom.thy	Sat Oct 10 16:21:34 2015 +0200
    15.2 +++ b/src/HOL/Algebra/RingHom.thy	Sat Oct 10 16:26:23 2015 +0200
    15.3 @@ -6,9 +6,9 @@
    15.4  imports Ideal
    15.5  begin
    15.6  
    15.7 -section {* Homomorphisms of Non-Commutative Rings *}
    15.8 +section \<open>Homomorphisms of Non-Commutative Rings\<close>
    15.9  
   15.10 -text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *}
   15.11 +text \<open>Lifting existing lemmas in a @{text ring_hom_ring} locale\<close>
   15.12  locale ring_hom_ring = R: ring R + S: ring S
   15.13      for R (structure) and S (structure) +
   15.14    fixes h
   15.15 @@ -100,7 +100,7 @@
   15.16  qed
   15.17  
   15.18  
   15.19 -subsection {* The Kernel of a Ring Homomorphism *}
   15.20 +subsection \<open>The Kernel of a Ring Homomorphism\<close>
   15.21  
   15.22  --"the kernel of a ring homomorphism is an ideal"
   15.23  lemma (in ring_hom_ring) kernel_is_ideal:
   15.24 @@ -111,15 +111,15 @@
   15.25   apply (unfold a_kernel_def', simp+)
   15.26  done
   15.27  
   15.28 -text {* Elements of the kernel are mapped to zero *}
   15.29 +text \<open>Elements of the kernel are mapped to zero\<close>
   15.30  lemma (in abelian_group_hom) kernel_zero [simp]:
   15.31    "i \<in> a_kernel R S h \<Longrightarrow> h i = \<zero>\<^bsub>S\<^esub>"
   15.32  by (simp add: a_kernel_defs)
   15.33  
   15.34  
   15.35 -subsection {* Cosets *}
   15.36 +subsection \<open>Cosets\<close>
   15.37  
   15.38 -text {* Cosets of the kernel correspond to the elements of the image of the homomorphism *}
   15.39 +text \<open>Cosets of the kernel correspond to the elements of the image of the homomorphism\<close>
   15.40  lemma (in ring_hom_ring) rcos_imp_homeq:
   15.41    assumes acarr: "a \<in> carrier R"
   15.42        and xrcos: "x \<in> a_kernel R S h +> a"
    16.1 --- a/src/HOL/Algebra/Sylow.thy	Sat Oct 10 16:21:34 2015 +0200
    16.2 +++ b/src/HOL/Algebra/Sylow.thy	Sat Oct 10 16:26:23 2015 +0200
    16.3 @@ -6,11 +6,11 @@
    16.4  imports Coset Exponent
    16.5  begin
    16.6  
    16.7 -text {*
    16.8 +text \<open>
    16.9    See also @{cite "Kammueller-Paulson:1999"}.
   16.10 -*}
   16.11 +\<close>
   16.12  
   16.13 -text{*The combinatorial argument is in theory Exponent*}
   16.14 +text\<open>The combinatorial argument is in theory Exponent\<close>
   16.15  
   16.16  locale sylow = group +
   16.17    fixes p and a and m and calM and RelM
   16.18 @@ -49,7 +49,7 @@
   16.19  done
   16.20  
   16.21  
   16.22 -subsection{*Main Part of the Proof*}
   16.23 +subsection\<open>Main Part of the Proof\<close>
   16.24  
   16.25  locale sylow_central = sylow +
   16.26    fixes H and M1 and M
   16.27 @@ -107,7 +107,7 @@
   16.28    qed
   16.29  
   16.30  
   16.31 -subsection{*Discharging the Assumptions of @{text sylow_central}*}
   16.32 +subsection\<open>Discharging the Assumptions of @{text sylow_central}\<close>
   16.33  
   16.34  lemma (in sylow) EmptyNotInEquivSet: "{} \<notin> calM // RelM"
   16.35  by (blast elim!: quotientE dest: RelM_equiv [THEN equiv_class_self])
   16.36 @@ -155,7 +155,7 @@
   16.37  done
   16.38  
   16.39  
   16.40 -subsubsection{*Introduction and Destruct Rules for @{term H}*}
   16.41 +subsubsection\<open>Introduction and Destruct Rules for @{term H}\<close>
   16.42  
   16.43  lemma (in sylow_central) H_I: "[|g \<in> carrier G; M1 #> g = M1|] ==> g \<in> H"
   16.44  by (simp add: H_def)
   16.45 @@ -216,10 +216,10 @@
   16.46  done
   16.47  
   16.48  
   16.49 -subsection{*Equal Cardinalities of @{term M} and the Set of Cosets*}
   16.50 +subsection\<open>Equal Cardinalities of @{term M} and the Set of Cosets\<close>
   16.51  
   16.52 -text{*Injections between @{term M} and @{term "rcosets\<^bsub>G\<^esub> H"} show that
   16.53 - their cardinalities are equal.*}
   16.54 +text\<open>Injections between @{term M} and @{term "rcosets\<^bsub>G\<^esub> H"} show that
   16.55 + their cardinalities are equal.\<close>
   16.56  
   16.57  lemma ElemClassEquiv:
   16.58       "[| equiv A r; C \<in> A // r |] ==> \<forall>x \<in> C. \<forall>y \<in> C. (x,y)\<in>r"
   16.59 @@ -259,7 +259,7 @@
   16.60  done
   16.61  
   16.62  
   16.63 -subsubsection{*The Opposite Injection*}
   16.64 +subsubsection\<open>The Opposite Injection\<close>
   16.65  
   16.66  lemma (in sylow_central) H_elem_map:
   16.67       "H1 \<in> rcosets H ==> \<exists>g. g \<in> carrier G & H #> g = H1"
   16.68 @@ -278,7 +278,7 @@
   16.69              intro!: M1_in_M in_quotient_imp_closed [OF RelM_equiv M_in_quot _  M1_RelM_rcosetGM1g])
   16.70  done
   16.71  
   16.72 -text{*close to a duplicate of @{text inj_M_GmodH}*}
   16.73 +text\<open>close to a duplicate of @{text inj_M_GmodH}\<close>
   16.74  lemma (in sylow_central) inj_GmodH_M:
   16.75       "\<exists>g \<in> rcosets H\<rightarrow>M. inj_on g (rcosets H)"
   16.76  apply (rule bexI)
   16.77 @@ -340,14 +340,14 @@
   16.78  apply (simp add: sylow_central_def sylow_central_axioms_def sylow_axioms calM_def RelM_def)
   16.79  done
   16.80  
   16.81 -text{*Needed because the locale's automatic definition refers to
   16.82 +text\<open>Needed because the locale's automatic definition refers to
   16.83     @{term "semigroup G"} and @{term "group_axioms G"} rather than
   16.84 -  simply to @{term "group G"}.*}
   16.85 +  simply to @{term "group G"}.\<close>
   16.86  lemma sylow_eq: "sylow G p a m = (group G & sylow_axioms G p a m)"
   16.87  by (simp add: sylow_def group_def)
   16.88  
   16.89  
   16.90 -subsection {* Sylow's Theorem *}
   16.91 +subsection \<open>Sylow's Theorem\<close>
   16.92  
   16.93  theorem sylow_thm:
   16.94       "[| prime p;  group(G);  order(G) = (p^a) * m; finite (carrier G)|]
    17.1 --- a/src/HOL/Algebra/UnivPoly.thy	Sat Oct 10 16:21:34 2015 +0200
    17.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Sat Oct 10 16:26:23 2015 +0200
    17.3 @@ -9,9 +9,9 @@
    17.4  imports Module RingHom
    17.5  begin
    17.6  
    17.7 -section {* Univariate Polynomials *}
    17.8 +section \<open>Univariate Polynomials\<close>
    17.9  
   17.10 -text {*
   17.11 +text \<open>
   17.12    Polynomials are formalised as modules with additional operations for
   17.13    extracting coefficients from polynomials and for obtaining monomials
   17.14    from coefficients and exponents (record @{text "up_ring"}).  The
   17.15 @@ -21,14 +21,14 @@
   17.16    formalisation of polynomials in the PhD thesis @{cite "Ballarin:1999"},
   17.17    which was implemented with axiomatic type classes.  This was later
   17.18    ported to Locales.
   17.19 -*}
   17.20 +\<close>
   17.21  
   17.22  
   17.23 -subsection {* The Constructor for Univariate Polynomials *}
   17.24 +subsection \<open>The Constructor for Univariate Polynomials\<close>
   17.25  
   17.26 -text {*
   17.27 +text \<open>
   17.28    Functions with finite support.
   17.29 -*}
   17.30 +\<close>
   17.31  
   17.32  locale bound =
   17.33    fixes z :: 'a
   17.34 @@ -67,9 +67,9 @@
   17.35     monom = (%a:carrier R. %n i. if i=n then a else \<zero>\<^bsub>R\<^esub>),
   17.36     coeff = (%p:up R. %n. p n)\<rparr>"
   17.37  
   17.38 -text {*
   17.39 +text \<open>
   17.40    Properties of the set of polynomials @{term up}.
   17.41 -*}
   17.42 +\<close>
   17.43  
   17.44  lemma mem_upI [intro]:
   17.45    "[| !!n. f n \<in> carrier R; EX n. bound (zero R) n f |] ==> f \<in> up R"
   17.46 @@ -168,7 +168,7 @@
   17.47  end
   17.48  
   17.49  
   17.50 -subsection {* Effect of Operations on Coefficients *}
   17.51 +subsection \<open>Effect of Operations on Coefficients\<close>
   17.52  
   17.53  locale UP =
   17.54    fixes R (structure) and P (structure)
   17.55 @@ -189,7 +189,7 @@
   17.56  context UP
   17.57  begin
   17.58  
   17.59 -text {*Temporarily declare @{thm P_def} as simp rule.*}
   17.60 +text \<open>Temporarily declare @{thm P_def} as simp rule.\<close>
   17.61  
   17.62  declare P_def [simp]
   17.63  
   17.64 @@ -240,12 +240,12 @@
   17.65  end
   17.66  
   17.67  
   17.68 -subsection {* Polynomials Form a Ring. *}
   17.69 +subsection \<open>Polynomials Form a Ring.\<close>
   17.70  
   17.71  context UP_ring
   17.72  begin
   17.73  
   17.74 -text {* Operations are closed over @{term P}. *}
   17.75 +text \<open>Operations are closed over @{term P}.\<close>
   17.76  
   17.77  lemma UP_mult_closed [simp]:
   17.78    "[| p \<in> carrier P; q \<in> carrier P |] ==> p \<otimes>\<^bsub>P\<^esub> q \<in> carrier P" by (simp add: UP_def up_mult_closed)
   17.79 @@ -269,7 +269,7 @@
   17.80  
   17.81  declare (in UP) P_def [simp del]
   17.82  
   17.83 -text {* Algebraic ring properties *}
   17.84 +text \<open>Algebraic ring properties\<close>
   17.85  
   17.86  context UP_ring
   17.87  begin
   17.88 @@ -398,7 +398,7 @@
   17.89  end
   17.90  
   17.91  
   17.92 -subsection {* Polynomials Form a Commutative Ring. *}
   17.93 +subsection \<open>Polynomials Form a Commutative Ring.\<close>
   17.94  
   17.95  context UP_cring
   17.96  begin
   17.97 @@ -428,7 +428,7 @@
   17.98  qed (simp_all add: R1 R2)
   17.99  
  17.100  
  17.101 -subsection {*Polynomials over a commutative ring for a commutative ring*}
  17.102 +subsection \<open>Polynomials over a commutative ring for a commutative ring\<close>
  17.103  
  17.104  theorem UP_cring:
  17.105    "cring P" using UP_ring unfolding cring_def by (auto intro!: comm_monoidI UP_m_assoc UP_m_comm)
  17.106 @@ -461,7 +461,7 @@
  17.107  sublocale UP_cring < P: cring P using UP_cring .
  17.108  
  17.109  
  17.110 -subsection {* Polynomials Form an Algebra *}
  17.111 +subsection \<open>Polynomials Form an Algebra\<close>
  17.112  
  17.113  context UP_ring
  17.114  begin
  17.115 @@ -496,9 +496,9 @@
  17.116  
  17.117  end
  17.118  
  17.119 -text {*
  17.120 +text \<open>
  17.121    Interpretation of lemmas from @{term algebra}.
  17.122 -*}
  17.123 +\<close>
  17.124  
  17.125  lemma (in cring) cring:
  17.126    "cring R" ..
  17.127 @@ -510,7 +510,7 @@
  17.128  sublocale UP_cring < algebra R P using UP_algebra .
  17.129  
  17.130  
  17.131 -subsection {* Further Lemmas Involving Monomials *}
  17.132 +subsection \<open>Further Lemmas Involving Monomials\<close>
  17.133  
  17.134  context UP_ring
  17.135  begin
  17.136 @@ -637,8 +637,8 @@
  17.137    }
  17.138  qed
  17.139  
  17.140 -text{*The following corollary follows from lemmas @{thm "monom_one_Suc"} 
  17.141 -  and @{thm "monom_one_Suc2"}, and is trivial in @{term UP_cring}*}
  17.142 +text\<open>The following corollary follows from lemmas @{thm "monom_one_Suc"} 
  17.143 +  and @{thm "monom_one_Suc2"}, and is trivial in @{term UP_cring}\<close>
  17.144  
  17.145  corollary monom_one_comm: shows "monom P \<one> k \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k"
  17.146    unfolding monom_one_Suc [symmetric] monom_one_Suc2 [symmetric] ..
  17.147 @@ -709,7 +709,7 @@
  17.148  end
  17.149  
  17.150  
  17.151 -subsection {* The Degree Function *}
  17.152 +subsection \<open>The Degree Function\<close>
  17.153  
  17.154  definition
  17.155    deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
  17.156 @@ -743,19 +743,19 @@
  17.157    assumes "deg R p < m" and "p \<in> carrier P"
  17.158    shows "coeff P p m = \<zero>"
  17.159  proof -
  17.160 -  from `p \<in> carrier P` obtain n where "bound \<zero> n (coeff P p)"
  17.161 +  from \<open>p \<in> carrier P\<close> obtain n where "bound \<zero> n (coeff P p)"
  17.162      by (auto simp add: UP_def P_def)
  17.163    then have "bound \<zero> (deg R p) (coeff P p)"
  17.164      by (auto simp: deg_def P_def dest: LeastI)
  17.165 -  from this and `deg R p < m` show ?thesis ..
  17.166 +  from this and \<open>deg R p < m\<close> show ?thesis ..
  17.167  qed
  17.168  
  17.169  lemma deg_belowI:
  17.170    assumes non_zero: "n ~= 0 ==> coeff P p n ~= \<zero>"
  17.171      and R: "p \<in> carrier P"
  17.172    shows "n <= deg R p"
  17.173 --- {* Logically, this is a slightly stronger version of
  17.174 -   @{thm [source] deg_aboveD} *}
  17.175 +-- \<open>Logically, this is a slightly stronger version of
  17.176 +   @{thm [source] deg_aboveD}\<close>
  17.177  proof (cases "n=0")
  17.178    case True then show ?thesis by simp
  17.179  next
  17.180 @@ -814,7 +814,7 @@
  17.181        !!n. n ~= 0 ==> coeff P p n ~= \<zero>; p \<in> carrier P |] ==> deg R p = n"
  17.182  by (fast intro: le_antisym deg_aboveI deg_belowI)
  17.183  
  17.184 -text {* Degree and polynomial operations *}
  17.185 +text \<open>Degree and polynomial operations\<close>
  17.186  
  17.187  lemma deg_add [simp]:
  17.188    "p \<in> carrier P \<Longrightarrow> q \<in> carrier P \<Longrightarrow>
  17.189 @@ -863,8 +863,8 @@
  17.190        inj_on_iff [OF R.a_inv_inj, of _ "\<zero>", simplified] R)
  17.191  qed
  17.192  
  17.193 -text{*The following lemma is later \emph{overwritten} by the most
  17.194 -  specific one for domains, @{text deg_smult}.*}
  17.195 +text\<open>The following lemma is later \emph{overwritten} by the most
  17.196 +  specific one for domains, @{text deg_smult}.\<close>
  17.197  
  17.198  lemma deg_smult_ring [simp]:
  17.199    "[| a \<in> carrier R; p \<in> carrier P |] ==>
  17.200 @@ -949,7 +949,7 @@
  17.201  
  17.202  end
  17.203  
  17.204 -text{*The following lemmas also can be lifted to @{term UP_ring}.*}
  17.205 +text\<open>The following lemmas also can be lifted to @{term UP_ring}.\<close>
  17.206  
  17.207  context UP_ring
  17.208  begin
  17.209 @@ -1013,7 +1013,7 @@
  17.210  end
  17.211  
  17.212  
  17.213 -subsection {* Polynomials over Integral Domains *}
  17.214 +subsection \<open>Polynomials over Integral Domains\<close>
  17.215  
  17.216  lemma domainI:
  17.217    assumes cring: "cring R"
  17.218 @@ -1071,15 +1071,15 @@
  17.219  
  17.220  end
  17.221  
  17.222 -text {*
  17.223 +text \<open>
  17.224    Interpretation of theorems from @{term domain}.
  17.225 -*}
  17.226 +\<close>
  17.227  
  17.228  sublocale UP_domain < "domain" P
  17.229    by intro_locales (rule domain.axioms UP_domain)+
  17.230  
  17.231  
  17.232 -subsection {* The Evaluation Homomorphism and Universal Property*}
  17.233 +subsection \<open>The Evaluation Homomorphism and Universal Property\<close>
  17.234  
  17.235  (* alternative congruence rule (possibly more efficient)
  17.236  lemma (in abelian_monoid) finsum_cong2:
  17.237 @@ -1192,7 +1192,7 @@
  17.238  
  17.239  end
  17.240  
  17.241 -text {* The universal property of the polynomial ring *}
  17.242 +text \<open>The universal property of the polynomial ring\<close>
  17.243  
  17.244  locale UP_pre_univ_prop = ring_hom_cring + UP_cring
  17.245  
  17.246 @@ -1203,9 +1203,9 @@
  17.247    assumes indet_img_carrier [simp, intro]: "s \<in> carrier S"
  17.248    defines Eval_def: "Eval == eval R S h s"
  17.249  
  17.250 -text{*JE: I have moved the following lemma from Ring.thy and lifted then to the locale @{term ring_hom_ring} from @{term ring_hom_cring}.*}
  17.251 -text{*JE: I was considering using it in @{text eval_ring_hom}, but that property does not hold for non commutative rings, so 
  17.252 -  maybe it is not that necessary.*}
  17.253 +text\<open>JE: I have moved the following lemma from Ring.thy and lifted then to the locale @{term ring_hom_ring} from @{term ring_hom_cring}.\<close>
  17.254 +text\<open>JE: I was considering using it in @{text eval_ring_hom}, but that property does not hold for non commutative rings, so 
  17.255 +  maybe it is not that necessary.\<close>
  17.256  
  17.257  lemma (in ring_hom_ring) hom_finsum [simp]:
  17.258    "f \<in> A -> carrier R ==>
  17.259 @@ -1296,18 +1296,18 @@
  17.260    qed
  17.261  qed
  17.262  
  17.263 -text {*
  17.264 +text \<open>
  17.265    The following lemma could be proved in @{text UP_cring} with the additional
  17.266 -  assumption that @{text h} is closed. *}
  17.267 +  assumption that @{text h} is closed.\<close>
  17.268  
  17.269  lemma (in UP_pre_univ_prop) eval_const:
  17.270    "[| s \<in> carrier S; r \<in> carrier R |] ==> eval R S h s (monom P r 0) = h r"
  17.271    by (simp only: eval_on_carrier monom_closed) simp
  17.272  
  17.273 -text {* Further properties of the evaluation homomorphism. *}
  17.274 +text \<open>Further properties of the evaluation homomorphism.\<close>
  17.275  
  17.276 -text {* The following proof is complicated by the fact that in arbitrary
  17.277 -  rings one might have @{term "one R = zero R"}. *}
  17.278 +text \<open>The following proof is complicated by the fact that in arbitrary
  17.279 +  rings one might have @{term "one R = zero R"}.\<close>
  17.280  
  17.281  (* TODO: simplify by cases "one R = zero R" *)
  17.282  
  17.283 @@ -1336,7 +1336,7 @@
  17.284  
  17.285  end
  17.286  
  17.287 -text {* Interpretation of ring homomorphism lemmas. *}
  17.288 +text \<open>Interpretation of ring homomorphism lemmas.\<close>
  17.289  
  17.290  sublocale UP_univ_prop < ring_hom_cring P S Eval
  17.291    unfolding Eval_def
  17.292 @@ -1442,7 +1442,7 @@
  17.293  
  17.294  end
  17.295  
  17.296 -text{*JE: The following lemma was added by me; it might be even lifted to a simpler locale*}
  17.297 +text\<open>JE: The following lemma was added by me; it might be even lifted to a simpler locale\<close>
  17.298  
  17.299  context monoid
  17.300  begin
  17.301 @@ -1461,7 +1461,7 @@
  17.302    using lcoeff_nonzero [OF p_not_zero p_in_R] .
  17.303  
  17.304  
  17.305 -subsection{*The long division algorithm: some previous facts.*}
  17.306 +subsection\<open>The long division algorithm: some previous facts.\<close>
  17.307  
  17.308  lemma coeff_minus [simp]:
  17.309    assumes p: "p \<in> carrier P" and q: "q \<in> carrier P" shows "coeff P (p \<ominus>\<^bsub>P\<^esub> q) n = coeff P p n \<ominus> coeff P q n" 
  17.310 @@ -1538,7 +1538,7 @@
  17.311  end
  17.312  
  17.313  
  17.314 -subsection {* The long division proof for commutative rings *}
  17.315 +subsection \<open>The long division proof for commutative rings\<close>
  17.316  
  17.317  context UP_cring
  17.318  begin
  17.319 @@ -1547,7 +1547,7 @@
  17.320    shows "\<exists> x y z. Pred x y z"
  17.321    using exist by blast
  17.322  
  17.323 -text {* Jacobson's Theorem 2.14 *}
  17.324 +text \<open>Jacobson's Theorem 2.14\<close>
  17.325  
  17.326  lemma long_div_theorem: 
  17.327    assumes g_in_P [simp]: "g \<in> carrier P" and f_in_P [simp]: "f \<in> carrier P"
  17.328 @@ -1648,7 +1648,7 @@
  17.329  end
  17.330  
  17.331  
  17.332 -text {*The remainder theorem as corollary of the long division theorem.*}
  17.333 +text \<open>The remainder theorem as corollary of the long division theorem.\<close>
  17.334  
  17.335  context UP_cring
  17.336  begin
  17.337 @@ -1797,7 +1797,7 @@
  17.338  end
  17.339  
  17.340  
  17.341 -subsection {* Sample Application of Evaluation Homomorphism *}
  17.342 +subsection \<open>Sample Application of Evaluation Homomorphism\<close>
  17.343  
  17.344  lemma UP_pre_univ_propI:
  17.345    assumes "cring R"
  17.346 @@ -1820,11 +1820,11 @@
  17.347    "UP_pre_univ_prop INTEG INTEG id"
  17.348    by (fast intro: UP_pre_univ_propI INTEG_cring id_ring_hom)
  17.349  
  17.350 -text {*
  17.351 +text \<open>
  17.352    Interpretation now enables to import all theorems and lemmas
  17.353    valid in the context of homomorphisms between @{term INTEG} and @{term
  17.354    "UP INTEG"} globally.
  17.355 -*}
  17.356 +\<close>
  17.357  
  17.358  interpretation INTEG: UP_pre_univ_prop INTEG INTEG id "UP INTEG"
  17.359    using INTEG_id_eval by simp_all
    18.1 --- a/src/HOL/Old_Number_Theory/BijectionRel.thy	Sat Oct 10 16:21:34 2015 +0200
    18.2 +++ b/src/HOL/Old_Number_Theory/BijectionRel.thy	Sat Oct 10 16:26:23 2015 +0200
    18.3 @@ -3,18 +3,18 @@
    18.4      Copyright   2000  University of Cambridge
    18.5  *)
    18.6  
    18.7 -section {* Bijections between sets *}
    18.8 +section \<open>Bijections between sets\<close>
    18.9  
   18.10  theory BijectionRel
   18.11  imports Main
   18.12  begin
   18.13  
   18.14 -text {*
   18.15 +text \<open>
   18.16    Inductive definitions of bijections between two different sets and
   18.17    between the same set.  Theorem for relating the two definitions.
   18.18  
   18.19    \bigskip
   18.20 -*}
   18.21 +\<close>
   18.22  
   18.23  inductive_set
   18.24    bijR :: "('a => 'b => bool) => ('a set * 'b set) set"
   18.25 @@ -24,10 +24,10 @@
   18.26  | insert: "P a b ==> a \<notin> A ==> b \<notin> B ==> (A, B) \<in> bijR P
   18.27      ==> (insert a A, insert b B) \<in> bijR P"
   18.28  
   18.29 -text {*
   18.30 +text \<open>
   18.31    Add extra condition to @{term insert}: @{term "\<forall>b \<in> B. \<not> P a b"}
   18.32    (and similar for @{term A}).
   18.33 -*}
   18.34 +\<close>
   18.35  
   18.36  definition
   18.37    bijP :: "('a => 'a => bool) => 'a set => bool" where
   18.38 @@ -51,7 +51,7 @@
   18.39      ==> insert a (insert b A) \<in> bijER P"
   18.40  
   18.41  
   18.42 -text {* \medskip @{term bijR} *}
   18.43 +text \<open>\medskip @{term bijR}\<close>
   18.44  
   18.45  lemma fin_bijRl: "(A, B) \<in> bijR P ==> finite A"
   18.46    apply (erule bijR.induct)
   18.47 @@ -100,7 +100,7 @@
   18.48    done
   18.49  
   18.50  
   18.51 -text {* \medskip @{term bijER} *}
   18.52 +text \<open>\medskip @{term bijER}\<close>
   18.53  
   18.54  lemma fin_bijER: "A \<in> bijER P ==> finite A"
   18.55    apply (erule bijER.induct)
    19.1 --- a/src/HOL/Old_Number_Theory/Chinese.thy	Sat Oct 10 16:21:34 2015 +0200
    19.2 +++ b/src/HOL/Old_Number_Theory/Chinese.thy	Sat Oct 10 16:26:23 2015 +0200
    19.3 @@ -3,22 +3,22 @@
    19.4      Copyright   2000  University of Cambridge
    19.5  *)
    19.6  
    19.7 -section {* The Chinese Remainder Theorem *}
    19.8 +section \<open>The Chinese Remainder Theorem\<close>
    19.9  
   19.10  theory Chinese 
   19.11  imports IntPrimes
   19.12  begin
   19.13  
   19.14 -text {*
   19.15 +text \<open>
   19.16    The Chinese Remainder Theorem for an arbitrary finite number of
   19.17    equations.  (The one-equation case is included in theory @{text
   19.18    IntPrimes}.  Uses functions for indexing.\footnote{Maybe @{term
   19.19    funprod} and @{term funsum} should be based on general @{term fold}
   19.20    on indices?}
   19.21 -*}
   19.22 +\<close>
   19.23  
   19.24  
   19.25 -subsection {* Definitions *}
   19.26 +subsection \<open>Definitions\<close>
   19.27  
   19.28  primrec funprod :: "(nat => int) => nat => nat => int"
   19.29  where
   19.30 @@ -65,7 +65,7 @@
   19.31    "x_sol n kf bf mf = funsum (\<lambda>i. xilin_sol i n kf bf mf * mhf mf n i) 0 n"
   19.32  
   19.33  
   19.34 -text {* \medskip @{term funprod} and @{term funsum} *}
   19.35 +text \<open>\medskip @{term funprod} and @{term funsum}\<close>
   19.36  
   19.37  lemma funprod_pos: "(\<forall>i. i \<le> n --> 0 < mf i) ==> 0 < funprod mf 0 n"
   19.38  by (induct n) auto
   19.39 @@ -126,7 +126,7 @@
   19.40    done
   19.41  
   19.42  
   19.43 -subsection {* Chinese: uniqueness *}
   19.44 +subsection \<open>Chinese: uniqueness\<close>
   19.45  
   19.46  lemma zcong_funprod_aux:
   19.47    "m_cond n mf ==> km_cond n kf mf
   19.48 @@ -160,17 +160,17 @@
   19.49    done
   19.50  
   19.51  
   19.52 -subsection {* Chinese: existence *}
   19.53 +subsection \<open>Chinese: existence\<close>
   19.54  
   19.55  lemma unique_xi_sol:
   19.56    "0 < n ==> i \<le> n ==> m_cond n mf ==> km_cond n kf mf
   19.57      ==> \<exists>!x. 0 \<le> x \<and> x < mf i \<and> [kf i * mhf mf n i * x = bf i] (mod mf i)"
   19.58    apply (rule zcong_lineq_unique)
   19.59 -   apply (tactic {* stac @{context} @{thm zgcd_zmult_cancel} 2 *})
   19.60 +   apply (tactic \<open>stac @{context} @{thm zgcd_zmult_cancel} 2\<close>)
   19.61      apply (unfold m_cond_def km_cond_def mhf_def)
   19.62      apply (simp_all (no_asm_simp))
   19.63    apply safe
   19.64 -    apply (tactic {* stac @{context} @{thm zgcd_zmult_cancel} 3 *})
   19.65 +    apply (tactic \<open>stac @{context} @{thm zgcd_zmult_cancel} 3\<close>)
   19.66       apply (rule_tac [!] funprod_zgcd)
   19.67       apply safe
   19.68       apply simp_all
   19.69 @@ -216,7 +216,7 @@
   19.70    done
   19.71  
   19.72  
   19.73 -subsection {* Chinese *}
   19.74 +subsection \<open>Chinese\<close>
   19.75  
   19.76  lemma chinese_remainder:
   19.77    "0 < n ==> m_cond n mf ==> km_cond n kf mf
   19.78 @@ -228,19 +228,19 @@
   19.79    apply (rule_tac x = "x_sol n kf bf mf mod funprod mf 0 n" in exI)
   19.80    apply (unfold lincong_sol_def)
   19.81    apply safe
   19.82 -    apply (tactic {* stac @{context} @{thm zcong_zmod} 3 *})
   19.83 -    apply (tactic {* stac @{context} @{thm mod_mult_eq} 3 *})
   19.84 -    apply (tactic {* stac @{context} @{thm mod_mod_cancel} 3 *})
   19.85 -      apply (tactic {* stac @{context} @{thm x_sol_lin} 4 *})
   19.86 -        apply (tactic {* stac @{context} (@{thm mod_mult_eq} RS sym) 6 *})
   19.87 -        apply (tactic {* stac @{context} (@{thm zcong_zmod} RS sym) 6 *})
   19.88 +    apply (tactic \<open>stac @{context} @{thm zcong_zmod} 3\<close>)
   19.89 +    apply (tactic \<open>stac @{context} @{thm mod_mult_eq} 3\<close>)
   19.90 +    apply (tactic \<open>stac @{context} @{thm mod_mod_cancel} 3\<close>)
   19.91 +      apply (tactic \<open>stac @{context} @{thm x_sol_lin} 4\<close>)
   19.92 +        apply (tactic \<open>stac @{context} (@{thm mod_mult_eq} RS sym) 6\<close>)
   19.93 +        apply (tactic \<open>stac @{context} (@{thm zcong_zmod} RS sym) 6\<close>)
   19.94          apply (subgoal_tac [6]
   19.95            "0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
   19.96            \<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
   19.97           prefer 6
   19.98           apply (simp add: ac_simps)
   19.99          apply (unfold xilin_sol_def)
  19.100 -        apply (tactic {* asm_simp_tac @{context} 6 *})
  19.101 +        apply (tactic \<open>asm_simp_tac @{context} 6\<close>)
  19.102          apply (rule_tac [6] ex1_implies_ex [THEN someI_ex])
  19.103          apply (rule_tac [6] unique_xi_sol)
  19.104             apply (rule_tac [3] funprod_zdvd)
    20.1 --- a/src/HOL/Old_Number_Theory/Euler.thy	Sat Oct 10 16:21:34 2015 +0200
    20.2 +++ b/src/HOL/Old_Number_Theory/Euler.thy	Sat Oct 10 16:26:23 2015 +0200
    20.3 @@ -2,7 +2,7 @@
    20.4      Authors:    Jeremy Avigad, David Gray, and Adam Kramer
    20.5  *)
    20.6  
    20.7 -section {* Euler's criterion *}
    20.8 +section \<open>Euler's criterion\<close>
    20.9  
   20.10  theory Euler
   20.11  imports Residues EvenOdd
   20.12 @@ -15,7 +15,7 @@
   20.13    where "SetS a p = MultInvPair a p ` SRStar p"
   20.14  
   20.15  
   20.16 -subsection {* Property for MultInvPair *}
   20.17 +subsection \<open>Property for MultInvPair\<close>
   20.18  
   20.19  lemma MultInvPair_prop1a:
   20.20    "[| zprime p; 2 < p; ~([a = 0](mod p));
   20.21 @@ -89,7 +89,7 @@
   20.22    done
   20.23  
   20.24  
   20.25 -subsection {* Properties of SetS *}
   20.26 +subsection \<open>Properties of SetS\<close>
   20.27  
   20.28  lemma SetS_finite: "2 < p ==> finite (SetS a p)"
   20.29    by (auto simp add: SetS_def SRStar_finite [of p])
   20.30 @@ -223,14 +223,14 @@
   20.31    apply (auto simp add: Union_SetS_setprod_prop2)
   20.32    done
   20.33  
   20.34 -text {* \medskip Prove the first part of Euler's Criterion: *}
   20.35 +text \<open>\medskip Prove the first part of Euler's Criterion:\<close>
   20.36  
   20.37  lemma Euler_part1: "[| 2 < p; zprime p; ~([x = 0](mod p)); 
   20.38      ~(QuadRes p x) |] ==> 
   20.39        [x^(nat (((p) - 1) div 2)) = -1](mod p)"
   20.40    by (metis Wilson_Russ zcong_sym zcong_trans zfact_prop)
   20.41  
   20.42 -text {* \medskip Prove another part of Euler Criterion: *}
   20.43 +text \<open>\medskip Prove another part of Euler Criterion:\<close>
   20.44  
   20.45  lemma aux_1: "0 < p ==> (a::int) ^ nat (p) = a * a ^ (nat (p) - 1)"
   20.46  proof -
   20.47 @@ -251,7 +251,7 @@
   20.48      by (auto simp add: zEven_def zOdd_def)
   20.49    then have aux_1: "2 * ((p - 1) div 2) = (p - 1)"
   20.50      by (auto simp add: even_div_2_prop2)
   20.51 -  with `2 < p` have "1 < (p - 1)"
   20.52 +  with \<open>2 < p\<close> have "1 < (p - 1)"
   20.53      by auto
   20.54    then have " 1 < (2 * ((p - 1) div 2))"
   20.55      by (auto simp add: aux_1)
   20.56 @@ -268,7 +268,7 @@
   20.57    apply (frule zcong_zmult_prop1, auto)
   20.58    done
   20.59  
   20.60 -text {* \medskip Prove the final part of Euler's Criterion: *}
   20.61 +text \<open>\medskip Prove the final part of Euler's Criterion:\<close>
   20.62  
   20.63  lemma aux__1: "[| ~([x = 0] (mod p)); [y\<^sup>2 = x] (mod p)|] ==> ~(p dvd y)"
   20.64    by (metis dvdI power2_eq_square zcong_sym zcong_trans zcong_zero_equiv_div dvd_trans)
   20.65 @@ -291,7 +291,7 @@
   20.66    done
   20.67  
   20.68  
   20.69 -text {* \medskip Finally show Euler's Criterion: *}
   20.70 +text \<open>\medskip Finally show Euler's Criterion:\<close>
   20.71  
   20.72  theorem Euler_Criterion: "[| 2 < p; zprime p |] ==> [(Legendre a p) =
   20.73      a^(nat (((p) - 1) div 2))] (mod p)"
    21.1 --- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Sat Oct 10 16:21:34 2015 +0200
    21.2 +++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Sat Oct 10 16:26:23 2015 +0200
    21.3 @@ -3,20 +3,20 @@
    21.4      Copyright   2000  University of Cambridge
    21.5  *)
    21.6  
    21.7 -section {* Fermat's Little Theorem extended to Euler's Totient function *}
    21.8 +section \<open>Fermat's Little Theorem extended to Euler's Totient function\<close>
    21.9  
   21.10  theory EulerFermat
   21.11  imports BijectionRel IntFact
   21.12  begin
   21.13  
   21.14 -text {*
   21.15 +text \<open>
   21.16    Fermat's Little Theorem extended to Euler's Totient function. More
   21.17    abstract approach than Boyer-Moore (which seems necessary to achieve
   21.18    the extended version).
   21.19 -*}
   21.20 +\<close>
   21.21  
   21.22  
   21.23 -subsection {* Definitions and lemmas *}
   21.24 +subsection \<open>Definitions and lemmas\<close>
   21.25  
   21.26  inductive_set RsetR :: "int => int set set" for m :: int
   21.27  where
   21.28 @@ -54,11 +54,11 @@
   21.29    where "zcongm m = (\<lambda>a b. zcong a b m)"
   21.30  
   21.31  lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)"
   21.32 -  -- {* LCP: not sure why this lemma is needed now *}
   21.33 +  -- \<open>LCP: not sure why this lemma is needed now\<close>
   21.34    by (auto simp add: abs_if)
   21.35  
   21.36  
   21.37 -text {* \medskip @{text norRRset} *}
   21.38 +text \<open>\medskip @{text norRRset}\<close>
   21.39  
   21.40  declare BnorRset.simps [simp del]
   21.41  
   21.42 @@ -146,7 +146,7 @@
   21.43    done
   21.44  
   21.45  
   21.46 -text {* \medskip @{term noXRRset} *}
   21.47 +text \<open>\medskip @{term noXRRset}\<close>
   21.48  
   21.49  lemma RRset_gcd [rule_format]:
   21.50      "is_RRset A m ==> a \<in> A --> zgcd a m = 1"
   21.51 @@ -249,7 +249,7 @@
   21.52        \<Prod>(BnorRset a m) * x^card (BnorRset a m)"
   21.53    apply (induct a m rule: BnorRset_induct)
   21.54     prefer 2
   21.55 -   apply (simplesubst BnorRset.simps)  --{*multiple redexes*}
   21.56 +   apply (simplesubst BnorRset.simps)  --\<open>multiple redexes\<close>
   21.57     apply (unfold Let_def, auto)
   21.58    apply (simp add: Bnor_fin Bnor_mem_zle_swap)
   21.59    apply (subst setprod.insert)
   21.60 @@ -259,7 +259,7 @@
   21.61    done
   21.62  
   21.63  
   21.64 -subsection {* Fermat *}
   21.65 +subsection \<open>Fermat\<close>
   21.66  
   21.67  lemma bijzcong_zcong_prod:
   21.68      "(A, B) \<in> bijR (zcongm m) ==> [\<Prod>A = \<Prod>B] (mod m)"
    22.1 --- a/src/HOL/Old_Number_Theory/EvenOdd.thy	Sat Oct 10 16:21:34 2015 +0200
    22.2 +++ b/src/HOL/Old_Number_Theory/EvenOdd.thy	Sat Oct 10 16:26:23 2015 +0200
    22.3 @@ -2,7 +2,7 @@
    22.4      Authors:    Jeremy Avigad, David Gray, and Adam Kramer
    22.5  *)
    22.6  
    22.7 -section {*Parity: Even and Odd Integers*}
    22.8 +section \<open>Parity: Even and Odd Integers\<close>
    22.9  
   22.10  theory EvenOdd
   22.11  imports Int2
   22.12 @@ -14,7 +14,7 @@
   22.13  definition zEven :: "int set"
   22.14    where "zEven = {x. \<exists>k. x = 2 * k}"
   22.15  
   22.16 -subsection {* Some useful properties about even and odd *}
   22.17 +subsection \<open>Some useful properties about even and odd\<close>
   22.18  
   22.19  lemma zOddI [intro?]: "x = 2 * k + 1 \<Longrightarrow> x \<in> zOdd"
   22.20    and zOddE [elim?]: "x \<in> zOdd \<Longrightarrow> (!!k. x = 2 * k + 1 \<Longrightarrow> C) \<Longrightarrow> C"
   22.21 @@ -167,11 +167,11 @@
   22.22  lemma neg_one_even_power: "[| x \<in> zEven; 0 \<le> x |] ==> (-1::int)^(nat x) = 1"
   22.23  proof -
   22.24    assume "x \<in> zEven" and "0 \<le> x"
   22.25 -  from `x \<in> zEven` obtain a where "x = 2 * a" ..
   22.26 -  with `0 \<le> x` have "0 \<le> a" by simp
   22.27 -  from `0 \<le> x` and `x = 2 * a` have "nat x = nat (2 * a)"
   22.28 +  from \<open>x \<in> zEven\<close> obtain a where "x = 2 * a" ..
   22.29 +  with \<open>0 \<le> x\<close> have "0 \<le> a" by simp
   22.30 +  from \<open>0 \<le> x\<close> and \<open>x = 2 * a\<close> have "nat x = nat (2 * a)"
   22.31      by simp
   22.32 -  also from `x = 2 * a` have "nat (2 * a) = 2 * nat a"
   22.33 +  also from \<open>x = 2 * a\<close> have "nat (2 * a) = 2 * nat a"
   22.34      by (simp add: nat_mult_distrib)
   22.35    finally have "(-1::int)^nat x = (-1)^(2 * nat a)"
   22.36      by simp
   22.37 @@ -186,9 +186,9 @@
   22.38  lemma neg_one_odd_power: "[| x \<in> zOdd; 0 \<le> x |] ==> (-1::int)^(nat x) = -1"
   22.39  proof -
   22.40    assume "x \<in> zOdd" and "0 \<le> x"
   22.41 -  from `x \<in> zOdd` obtain a where "x = 2 * a + 1" ..
   22.42 -  with `0 \<le> x` have a: "0 \<le> a" by simp
   22.43 -  with `0 \<le> x` and `x = 2 * a + 1` have "nat x = nat (2 * a + 1)"
   22.44 +  from \<open>x \<in> zOdd\<close> obtain a where "x = 2 * a + 1" ..
   22.45 +  with \<open>0 \<le> x\<close> have a: "0 \<le> a" by simp
   22.46 +  with \<open>0 \<le> x\<close> and \<open>x = 2 * a + 1\<close> have "nat x = nat (2 * a + 1)"
   22.47      by simp
   22.48    also from a have "nat (2 * a + 1) = 2 * nat a + 1"
   22.49      by (auto simp add: nat_mult_distrib nat_add_distrib)
   22.50 @@ -214,8 +214,8 @@
   22.51  lemma even_div_2_l: "[| y \<in> zEven; x < y |] ==> x div 2 < y div 2"
   22.52  proof -
   22.53    assume "y \<in> zEven" and "x < y"
   22.54 -  from `y \<in> zEven` obtain k where k: "y = 2 * k" ..
   22.55 -  with `x < y` have "x < 2 * k" by simp
   22.56 +  from \<open>y \<in> zEven\<close> obtain k where k: "y = 2 * k" ..
   22.57 +  with \<open>x < y\<close> have "x < 2 * k" by simp
   22.58    then have "x div 2 < k" by (auto simp add: div_prop1)
   22.59    also have "k = (2 * k) div 2" by simp
   22.60    finally have "x div 2 < 2 * k div 2" by simp
    23.1 --- a/src/HOL/Old_Number_Theory/Factorization.thy	Sat Oct 10 16:21:34 2015 +0200
    23.2 +++ b/src/HOL/Old_Number_Theory/Factorization.thy	Sat Oct 10 16:26:23 2015 +0200
    23.3 @@ -3,14 +3,14 @@
    23.4      Copyright   2000  University of Cambridge
    23.5  *)
    23.6  
    23.7 -section {* Fundamental Theorem of Arithmetic (unique factorization into primes) *}
    23.8 +section \<open>Fundamental Theorem of Arithmetic (unique factorization into primes)\<close>
    23.9  
   23.10  theory Factorization
   23.11  imports Primes "~~/src/HOL/Library/Permutation"
   23.12  begin
   23.13  
   23.14  
   23.15 -subsection {* Definitions *}
   23.16 +subsection \<open>Definitions\<close>
   23.17  
   23.18  definition primel :: "nat list => bool"
   23.19    where "primel xs = (\<forall>p \<in> set xs. prime p)"
   23.20 @@ -36,7 +36,7 @@
   23.21  | "sort (x # xs) = oinsert x (sort xs)"
   23.22  
   23.23  
   23.24 -subsection {* Arithmetic *}
   23.25 +subsection \<open>Arithmetic\<close>
   23.26  
   23.27  lemma one_less_m: "(m::nat) \<noteq> m * k ==> m \<noteq> Suc 0 ==> Suc 0 < m"
   23.28    apply (cases m)
   23.29 @@ -64,7 +64,7 @@
   23.30    done
   23.31  
   23.32  
   23.33 -subsection {* Prime list and product *}
   23.34 +subsection \<open>Prime list and product\<close>
   23.35  
   23.36  lemma prod_append: "prod (xs @ ys) = prod xs * prod ys"
   23.37    apply (induct xs)
   23.38 @@ -137,7 +137,7 @@
   23.39    done
   23.40  
   23.41  
   23.42 -subsection {* Sorting *}
   23.43 +subsection \<open>Sorting\<close>
   23.44  
   23.45  lemma nondec_oinsert: "nondec xs \<Longrightarrow> nondec (oinsert x xs)"
   23.46    apply (induct xs)
   23.47 @@ -174,7 +174,7 @@
   23.48    done
   23.49  
   23.50  
   23.51 -subsection {* Permutation *}
   23.52 +subsection \<open>Permutation\<close>
   23.53  
   23.54  lemma perm_primel [rule_format]: "xs <~~> ys ==> primel xs --> primel ys"
   23.55    apply (unfold primel_def)
   23.56 @@ -212,7 +212,7 @@
   23.57    done
   23.58  
   23.59  
   23.60 -subsection {* Existence *}
   23.61 +subsection \<open>Existence\<close>
   23.62  
   23.63  lemma ex_nondec_lemma:
   23.64      "primel xs ==> \<exists>ys. primel ys \<and> nondec ys \<and> prod ys = prod xs"
   23.65 @@ -250,7 +250,7 @@
   23.66    done
   23.67  
   23.68  
   23.69 -subsection {* Uniqueness *}
   23.70 +subsection \<open>Uniqueness\<close>
   23.71  
   23.72  lemma prime_dvd_mult_list [rule_format]:
   23.73      "prime p ==> p dvd (prod xs) --> (\<exists>m. m:set xs \<and> p dvd m)"
    24.1 --- a/src/HOL/Old_Number_Theory/Fib.thy	Sat Oct 10 16:21:34 2015 +0200
    24.2 +++ b/src/HOL/Old_Number_Theory/Fib.thy	Sat Oct 10 16:26:23 2015 +0200
    24.3 @@ -3,19 +3,19 @@
    24.4      Copyright   1997  University of Cambridge
    24.5  *)
    24.6  
    24.7 -section {* The Fibonacci function *}
    24.8 +section \<open>The Fibonacci function\<close>
    24.9  
   24.10  theory Fib
   24.11  imports Primes
   24.12  begin
   24.13  
   24.14 -text {*
   24.15 +text \<open>
   24.16    Fibonacci numbers: proofs of laws taken from:
   24.17    R. L. Graham, D. E. Knuth, O. Patashnik.  Concrete Mathematics.
   24.18    (Addison-Wesley, 1989)
   24.19  
   24.20    \bigskip
   24.21 -*}
   24.22 +\<close>
   24.23  
   24.24  fun fib :: "nat \<Rightarrow> nat"
   24.25  where
   24.26 @@ -23,21 +23,21 @@
   24.27  | "fib (Suc 0) = 1"
   24.28  | fib_2: "fib (Suc (Suc n)) = fib n + fib (Suc n)"
   24.29  
   24.30 -text {*
   24.31 +text \<open>
   24.32    \medskip The difficulty in these proofs is to ensure that the
   24.33    induction hypotheses are applied before the definition of @{term
   24.34    fib}.  Towards this end, the @{term fib} equations are not declared
   24.35    to the Simplifier and are applied very selectively at first.
   24.36 -*}
   24.37 +\<close>
   24.38  
   24.39 -text{*We disable @{text fib.fib_2fib_2} for simplification ...*}
   24.40 +text\<open>We disable @{text fib.fib_2fib_2} for simplification ...\<close>
   24.41  declare fib_2 [simp del]
   24.42  
   24.43 -text{*...then prove a version that has a more restrictive pattern.*}
   24.44 +text\<open>...then prove a version that has a more restrictive pattern.\<close>
   24.45  lemma fib_Suc3: "fib (Suc (Suc (Suc n))) = fib (Suc n) + fib (Suc (Suc n))"
   24.46    by (rule fib_2)
   24.47  
   24.48 -text {* \medskip Concrete Mathematics, page 280 *}
   24.49 +text \<open>\medskip Concrete Mathematics, page 280\<close>
   24.50  
   24.51  lemma fib_add: "fib (Suc (n + k)) = fib (Suc k) * fib (Suc n) + fib k * fib n"
   24.52  proof (induct n rule: fib.induct)
   24.53 @@ -60,10 +60,10 @@
   24.54    by (case_tac n, auto simp add: fib_Suc_gr_0) 
   24.55  
   24.56  
   24.57 -text {*
   24.58 +text \<open>
   24.59    \medskip Concrete Mathematics, page 278: Cassini's identity.  The proof is
   24.60    much easier using integers, not natural numbers!
   24.61 -*}
   24.62 +\<close>
   24.63  
   24.64  lemma fib_Cassini_int:
   24.65   "int (fib (Suc (Suc n)) * fib n) =
   24.66 @@ -79,8 +79,8 @@
   24.67    with "3.hyps" show ?case by (simp add: fib.simps add_mult_distrib add_mult_distrib2)
   24.68  qed
   24.69  
   24.70 -text{*We now obtain a version for the natural numbers via the coercion 
   24.71 -   function @{term int}.*}
   24.72 +text\<open>We now obtain a version for the natural numbers via the coercion 
   24.73 +   function @{term int}.\<close>
   24.74  theorem fib_Cassini:
   24.75   "fib (Suc (Suc n)) * fib n =
   24.76    (if n mod 2 = 0 then fib (Suc n) * fib (Suc n) - 1
   24.77 @@ -92,7 +92,7 @@
   24.78    done
   24.79  
   24.80  
   24.81 -text {* \medskip Toward Law 6.111 of Concrete Mathematics *}
   24.82 +text \<open>\medskip Toward Law 6.111 of Concrete Mathematics\<close>
   24.83  
   24.84  lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (Suc n)) = Suc 0"
   24.85    apply (induct n rule: fib.induct)
   24.86 @@ -135,7 +135,7 @@
   24.87    qed
   24.88  qed
   24.89  
   24.90 -lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"  -- {* Law 6.111 *}
   24.91 +lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"  -- \<open>Law 6.111\<close>
   24.92    apply (induct m n rule: gcd_induct)
   24.93    apply (simp_all add: gcd_non_0 gcd_commute gcd_fib_mod)
   24.94    done
    25.1 --- a/src/HOL/Old_Number_Theory/Finite2.thy	Sat Oct 10 16:21:34 2015 +0200
    25.2 +++ b/src/HOL/Old_Number_Theory/Finite2.thy	Sat Oct 10 16:26:23 2015 +0200
    25.3 @@ -2,19 +2,19 @@
    25.4      Authors:    Jeremy Avigad, David Gray, and Adam Kramer
    25.5  *)
    25.6  
    25.7 -section {*Finite Sets and Finite Sums*}
    25.8 +section \<open>Finite Sets and Finite Sums\<close>
    25.9  
   25.10  theory Finite2
   25.11  imports IntFact "~~/src/HOL/Library/Infinite_Set"
   25.12  begin
   25.13  
   25.14 -text{*
   25.15 +text\<open>
   25.16    These are useful for combinatorial and number-theoretic counting
   25.17    arguments.
   25.18 -*}
   25.19 +\<close>
   25.20  
   25.21  
   25.22 -subsection {* Useful properties of sums and products *}
   25.23 +subsection \<open>Useful properties of sums and products\<close>
   25.24  
   25.25  lemma setsum_same_function_zcong:
   25.26    assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
   25.27 @@ -48,7 +48,7 @@
   25.28    by (induct set: finite) (auto simp add: distrib_left)
   25.29  
   25.30  
   25.31 -subsection {* Cardinality of explicit finite sets *}
   25.32 +subsection \<open>Cardinality of explicit finite sets\<close>
   25.33  
   25.34  lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B"
   25.35  by (simp add: finite_subset)
   25.36 @@ -104,7 +104,7 @@
   25.37    also have "... = Suc (card {y. y < n})"
   25.38      by (rule card_insert_disjoint) (auto simp add: bdd_nat_set_l_finite)
   25.39    finally show "card {y. y < Suc n} = Suc n"
   25.40 -    using `card {y. y < n} = n` by simp
   25.41 +    using \<open>card {y. y < n} = n\<close> by simp
   25.42  qed
   25.43  
   25.44  lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x"
   25.45 @@ -121,7 +121,7 @@
   25.46      by (auto simp add: inj_on_def)
   25.47    hence "card (int ` {y. y < nat n}) = card {y. y < nat n}"
   25.48      by (rule card_image)
   25.49 -  also from `0 \<le> n` have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}"
   25.50 +  also from \<open>0 \<le> n\<close> have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}"
   25.51      apply (auto simp add: zless_nat_eq_int_zless image_def)
   25.52      apply (rule_tac x = "nat x" in exI)
   25.53      apply (auto simp add: nat_0_le)
   25.54 @@ -150,7 +150,7 @@
   25.55    hence "card ((%x. x+1) ` {x. 0 \<le> x & x < n}) =
   25.56       card {x. 0 \<le> x & x < n}"
   25.57      by (rule card_image)
   25.58 -  also from `0 \<le> n` have "... = nat n"
   25.59 +  also from \<open>0 \<le> n\<close> have "... = nat n"
   25.60      by (rule card_bdd_int_set_l)
   25.61    also have "(%x. x + 1) ` {x. 0 \<le> x & x < n} = {x. 0 < x & x<= n}"
   25.62      apply (auto simp add: image_def)
    26.1 --- a/src/HOL/Old_Number_Theory/Gauss.thy	Sat Oct 10 16:21:34 2015 +0200
    26.2 +++ b/src/HOL/Old_Number_Theory/Gauss.thy	Sat Oct 10 16:26:23 2015 +0200
    26.3 @@ -2,7 +2,7 @@
    26.4      Authors:    Jeremy Avigad, David Gray, and Adam Kramer
    26.5  *)
    26.6  
    26.7 -section {* Gauss' Lemma *}
    26.8 +section \<open>Gauss' Lemma\<close>
    26.9  
   26.10  theory Gauss
   26.11  imports Euler
   26.12 @@ -26,7 +26,7 @@
   26.13  definition "F = (%x. (p - x)) ` E"
   26.14  
   26.15  
   26.16 -subsection {* Basic properties of p *}
   26.17 +subsection \<open>Basic properties of p\<close>
   26.18  
   26.19  lemma p_odd: "p \<in> zOdd"
   26.20    by (auto simp add: p_prime p_g_2 zprime_zOdd_eq_grt_2)
   26.21 @@ -64,7 +64,7 @@
   26.22    done
   26.23  
   26.24  
   26.25 -subsection {* Basic Properties of the Gauss Sets *}
   26.26 +subsection \<open>Basic Properties of the Gauss Sets\<close>
   26.27  
   26.28  lemma finite_A: "finite (A)"
   26.29  by (auto simp add: A_def)
   26.30 @@ -272,7 +272,7 @@
   26.31  by(rule all_relprime_prod_relprime[OF finite_A all_A_relprime])
   26.32  
   26.33  
   26.34 -subsection {* Relationships Between Gauss Sets *}
   26.35 +subsection \<open>Relationships Between Gauss Sets\<close>
   26.36  
   26.37  lemma B_card_eq_A: "card B = card A"
   26.38    using finite_A by (simp add: finite_A B_def inj_on_xa_A card_image)
   26.39 @@ -434,7 +434,7 @@
   26.40  qed
   26.41  
   26.42  
   26.43 -subsection {* Gauss' Lemma *}
   26.44 +subsection \<open>Gauss' Lemma\<close>
   26.45  
   26.46  lemma aux: "setprod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = setprod id A * a ^ card A"
   26.47    by (auto simp add: finite_E neg_one_special)
    27.1 --- a/src/HOL/Old_Number_Theory/Int2.thy	Sat Oct 10 16:21:34 2015 +0200
    27.2 +++ b/src/HOL/Old_Number_Theory/Int2.thy	Sat Oct 10 16:26:23 2015 +0200
    27.3 @@ -2,7 +2,7 @@
    27.4      Authors:    Jeremy Avigad, David Gray, and Adam Kramer
    27.5  *)
    27.6  
    27.7 -section {*Integers: Divisibility and Congruences*}
    27.8 +section \<open>Integers: Divisibility and Congruences\<close>
    27.9  
   27.10  theory Int2
   27.11  imports Finite2 WilsonRuss
   27.12 @@ -12,7 +12,7 @@
   27.13    where "MultInv p x = x ^ nat (p - 2)"
   27.14  
   27.15  
   27.16 -subsection {* Useful lemmas about dvd and powers *}
   27.17 +subsection \<open>Useful lemmas about dvd and powers\<close>
   27.18  
   27.19  lemma zpower_zdvd_prop1:
   27.20    "0 < n \<Longrightarrow> p dvd y \<Longrightarrow> p dvd ((y::int) ^ n)"
   27.21 @@ -47,12 +47,12 @@
   27.22    assumes "0 < z" and "(x::int) < y * z"
   27.23    shows "x div z < y"
   27.24  proof -
   27.25 -  from `0 < z` have modth: "x mod z \<ge> 0" by simp
   27.26 +  from \<open>0 < z\<close> have modth: "x mod z \<ge> 0" by simp
   27.27    have "(x div z) * z \<le> (x div z) * z" by simp
   27.28    then have "(x div z) * z \<le> (x div z) * z + x mod z" using modth by arith 
   27.29    also have "\<dots> = x"
   27.30      by (auto simp add: zmod_zdiv_equality [symmetric] ac_simps)
   27.31 -  also note `x < y * z`
   27.32 +  also note \<open>x < y * z\<close>
   27.33    finally show ?thesis
   27.34      apply (auto simp add: mult_less_cancel_right)
   27.35      using assms apply arith
   27.36 @@ -66,7 +66,7 @@
   27.37    from assms have "x < (y + 1) * z" by (auto simp add: int_distrib)
   27.38    then have "x div z < y + 1"
   27.39      apply (rule_tac y = "y + 1" in div_prop1)
   27.40 -    apply (auto simp add: `0 < z`)
   27.41 +    apply (auto simp add: \<open>0 < z\<close>)
   27.42      done
   27.43    then show ?thesis by auto
   27.44  qed
   27.45 @@ -79,7 +79,7 @@
   27.46  qed
   27.47  
   27.48  
   27.49 -subsection {* Useful properties of congruences *}
   27.50 +subsection \<open>Useful properties of congruences\<close>
   27.51  
   27.52  lemma zcong_eq_zdvd_prop: "[x = 0](mod p) = (p dvd x)"
   27.53    by (auto simp add: zcong_def)
   27.54 @@ -142,7 +142,7 @@
   27.55      by auto
   27.56    then have "p dvd 2"
   27.57      by (auto simp add: dvd_def zcong_def)
   27.58 -  with `2 < p` show False
   27.59 +  with \<open>2 < p\<close> show False
   27.60      by (auto simp add: zdvd_not_zless)
   27.61  qed
   27.62  
   27.63 @@ -174,7 +174,7 @@
   27.64    by (induct set: finite) (auto simp add: zgcd_zgcd_zmult)
   27.65  
   27.66  
   27.67 -subsection {* Some properties of MultInv *}
   27.68 +subsection \<open>Some properties of MultInv\<close>
   27.69  
   27.70  lemma MultInv_prop1: "[| 2 < p; [x = y] (mod p) |] ==>
   27.71      [(MultInv p x) = (MultInv p y)] (mod p)"
    28.1 --- a/src/HOL/Old_Number_Theory/IntFact.thy	Sat Oct 10 16:21:34 2015 +0200
    28.2 +++ b/src/HOL/Old_Number_Theory/IntFact.thy	Sat Oct 10 16:26:23 2015 +0200
    28.3 @@ -3,19 +3,19 @@
    28.4      Copyright   2000  University of Cambridge
    28.5  *)
    28.6  
    28.7 -section {* Factorial on integers *}
    28.8 +section \<open>Factorial on integers\<close>
    28.9  
   28.10  theory IntFact
   28.11  imports IntPrimes
   28.12  begin
   28.13  
   28.14 -text {*
   28.15 +text \<open>
   28.16    Factorial on integers and recursively defined set including all
   28.17    Integers from @{text 2} up to @{text a}.  Plus definition of product
   28.18    of finite set.
   28.19  
   28.20    \bigskip
   28.21 -*}
   28.22 +\<close>
   28.23  
   28.24  fun zfact :: "int => int"
   28.25    where "zfact n = (if n \<le> 0 then 1 else n * zfact (n - 1))"
   28.26 @@ -24,10 +24,10 @@
   28.27    where "d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})"
   28.28  
   28.29  
   28.30 -text {*
   28.31 +text \<open>
   28.32    \medskip @{term d22set} --- recursively defined set including all
   28.33    integers from @{text 2} up to @{text a}
   28.34 -*}
   28.35 +\<close>
   28.36  
   28.37  declare d22set.simps [simp del]
   28.38  
    29.1 --- a/src/HOL/Old_Number_Theory/IntPrimes.thy	Sat Oct 10 16:21:34 2015 +0200
    29.2 +++ b/src/HOL/Old_Number_Theory/IntPrimes.thy	Sat Oct 10 16:26:23 2015 +0200
    29.3 @@ -3,22 +3,22 @@
    29.4      Copyright   2000  University of Cambridge
    29.5  *)
    29.6  
    29.7 -section {* Divisibility and prime numbers (on integers) *}
    29.8 +section \<open>Divisibility and prime numbers (on integers)\<close>
    29.9  
   29.10  theory IntPrimes
   29.11  imports Primes
   29.12  begin
   29.13  
   29.14 -text {*
   29.15 +text \<open>
   29.16    The @{text dvd} relation, GCD, Euclid's extended algorithm, primes,
   29.17    congruences (all on the Integers).  Comparable to theory @{text
   29.18    Primes}, but @{text dvd} is included here as it is not present in
   29.19    main HOL.  Also includes extended GCD and congruences not present in
   29.20    @{text Primes}.
   29.21 -*}
   29.22 +\<close>
   29.23  
   29.24  
   29.25 -subsection {* Definitions *}
   29.26 +subsection \<open>Definitions\<close>
   29.27  
   29.28  fun xzgcda :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int => (int * int * int)"
   29.29  where
   29.30 @@ -38,7 +38,7 @@
   29.31    where "[a = b] (mod m) = (m dvd (a - b))"
   29.32  
   29.33  
   29.34 -subsection {* Euclid's Algorithm and GCD *}
   29.35 +subsection \<open>Euclid's Algorithm and GCD\<close>
   29.36  
   29.37  
   29.38  lemma zrelprime_zdvd_zmult_aux:
   29.39 @@ -55,8 +55,8 @@
   29.40  lemma zgcd_geq_zero: "0 <= zgcd x y"
   29.41    by (auto simp add: zgcd_def)
   29.42  
   29.43 -text{*This is merely a sanity check on zprime, since the previous version
   29.44 -      denoted the empty set.*}
   29.45 +text\<open>This is merely a sanity check on zprime, since the previous version
   29.46 +      denoted the empty set.\<close>
   29.47  lemma "zprime 2"
   29.48    apply (auto simp add: zprime_def) 
   29.49    apply (frule zdvd_imp_le, simp) 
   29.50 @@ -109,7 +109,7 @@
   29.51  
   29.52  
   29.53  
   29.54 -subsection {* Congruences *}
   29.55 +subsection \<open>Congruences\<close>
   29.56  
   29.57  lemma zcong_1 [simp]: "[a = b] (mod 1)"
   29.58    by (unfold zcong_def, auto)
   29.59 @@ -281,7 +281,7 @@
   29.60    apply (simp add: linorder_neq_iff)
   29.61    apply (erule disjE)  
   29.62     prefer 2 apply (simp add: zcong_zmod_eq)
   29.63 -  txt{*Remainding case: @{term "m<0"}*}
   29.64 +  txt\<open>Remainding case: @{term "m<0"}\<close>
   29.65    apply (rule_tac t = m in minus_minus [THEN subst])
   29.66    apply (subst zcong_zminus)
   29.67    apply (subst zcong_zmod_eq, arith)
   29.68 @@ -289,14 +289,14 @@
   29.69    apply (simp add: zmod_zminus2_eq_if del: neg_mod_bound)
   29.70    done
   29.71  
   29.72 -subsection {* Modulo *}
   29.73 +subsection \<open>Modulo\<close>
   29.74  
   29.75  lemma zmod_zdvd_zmod:
   29.76      "0 < (m::int) ==> m dvd b ==> (a mod b mod m) = (a mod m)"
   29.77    by (rule mod_mod_cancel) 
   29.78  
   29.79  
   29.80 -subsection {* Extended GCD *}
   29.81 +subsection \<open>Extended GCD\<close>
   29.82  
   29.83  declare xzgcda.simps [simp del]
   29.84  
   29.85 @@ -336,7 +336,7 @@
   29.86    done
   29.87  
   29.88  
   29.89 -text {* \medskip @{term xzgcd} linear *}
   29.90 +text \<open>\medskip @{term xzgcd} linear\<close>
   29.91  
   29.92  lemma xzgcda_linear_aux1:
   29.93    "(a - r * b) * m + (c - r * d) * (n::int) =
   29.94 @@ -399,7 +399,7 @@
   29.95      zgcd a n = 1 ==> \<exists>!x. 0 \<le> x \<and> x < n \<and> [a * x = b] (mod n)"
   29.96    apply auto
   29.97     apply (rule_tac [2] zcong_zless_imp_eq)
   29.98 -       apply (tactic {* stac @{context} (@{thm zcong_cancel2} RS sym) 6 *})
   29.99 +       apply (tactic \<open>stac @{context} (@{thm zcong_cancel2} RS sym) 6\<close>)
  29.100           apply (rule_tac [8] zcong_trans)
  29.101            apply (simp_all (no_asm_simp))
  29.102     prefer 2
    30.1 --- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Sat Oct 10 16:21:34 2015 +0200
    30.2 +++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Sat Oct 10 16:26:23 2015 +0200
    30.3 @@ -3,40 +3,40 @@
    30.4      Copyright   1996  University of Cambridge
    30.5  *)
    30.6  
    30.7 -section {* The Greatest Common Divisor *}
    30.8 +section \<open>The Greatest Common Divisor\<close>
    30.9  
   30.10  theory Legacy_GCD
   30.11  imports Main
   30.12  begin
   30.13  
   30.14 -text {*
   30.15 +text \<open>
   30.16    See @{cite davenport92}. \bigskip
   30.17 -*}
   30.18 +\<close>
   30.19  
   30.20 -subsection {* Specification of GCD on nats *}
   30.21 +subsection \<open>Specification of GCD on nats\<close>
   30.22  
   30.23  definition
   30.24 -  is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- {* @{term gcd} as a relation *}
   30.25 +  is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- \<open>@{term gcd} as a relation\<close>
   30.26    "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
   30.27      (\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
   30.28  
   30.29 -text {* Uniqueness *}
   30.30 +text \<open>Uniqueness\<close>
   30.31  
   30.32  lemma is_gcd_unique: "is_gcd a b m \<Longrightarrow> is_gcd a b n \<Longrightarrow> m = n"
   30.33    by (simp add: is_gcd_def) (blast intro: dvd_antisym)
   30.34  
   30.35 -text {* Connection to divides relation *}
   30.36 +text \<open>Connection to divides relation\<close>
   30.37  
   30.38  lemma is_gcd_dvd: "is_gcd a b m \<Longrightarrow> k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd m"
   30.39    by (auto simp add: is_gcd_def)
   30.40  
   30.41 -text {* Commutativity *}
   30.42 +text \<open>Commutativity\<close>
   30.43  
   30.44  lemma is_gcd_commute: "is_gcd m n k = is_gcd n m k"
   30.45    by (auto simp add: is_gcd_def)
   30.46  
   30.47  
   30.48 -subsection {* GCD on nat by Euclid's algorithm *}
   30.49 +subsection \<open>GCD on nat by Euclid's algorithm\<close>
   30.50  
   30.51  fun gcd :: "nat => nat => nat"
   30.52    where "gcd m n = (if n = 0 then m else gcd n (m mod n))"
   30.53 @@ -68,10 +68,10 @@
   30.54  
   30.55  declare gcd.simps [simp del]
   30.56  
   30.57 -text {*
   30.58 +text \<open>
   30.59    \medskip @{term "gcd m n"} divides @{text m} and @{text n}.  The
   30.60    conjunctions don't seem provable separately.
   30.61 -*}
   30.62 +\<close>
   30.63  
   30.64  lemma gcd_dvd1 [iff, algebra]: "gcd m n dvd m"
   30.65    and gcd_dvd2 [iff, algebra]: "gcd m n dvd n"
   30.66 @@ -80,24 +80,24 @@
   30.67    apply (blast dest: dvd_mod_imp_dvd)
   30.68    done
   30.69  
   30.70 -text {*
   30.71 +text \<open>
   30.72    \medskip Maximality: for all @{term m}, @{term n}, @{term k}
   30.73    naturals, if @{term k} divides @{term m} and @{term k} divides
   30.74    @{term n} then @{term k} divides @{term "gcd m n"}.
   30.75 -*}
   30.76 +\<close>
   30.77  
   30.78  lemma gcd_greatest: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
   30.79    by (induct m n rule: gcd_induct) (simp_all add: gcd_non_0 dvd_mod)
   30.80  
   30.81 -text {*
   30.82 +text \<open>
   30.83    \medskip Function gcd yields the Greatest Common Divisor.
   30.84 -*}
   30.85 +\<close>
   30.86  
   30.87  lemma is_gcd: "is_gcd m n (gcd m n) "
   30.88    by (simp add: is_gcd_def gcd_greatest)
   30.89  
   30.90  
   30.91 -subsection {* Derived laws for GCD *}
   30.92 +subsection \<open>Derived laws for GCD\<close>
   30.93  
   30.94  lemma gcd_greatest_iff [iff, algebra]: "k dvd gcd m n \<longleftrightarrow> k dvd m \<and> k dvd n"
   30.95    by (blast intro!: gcd_greatest intro: dvd_trans)
   30.96 @@ -125,12 +125,12 @@
   30.97  lemma nat_gcd_1_left [simp, algebra]: "gcd 1 m = 1"
   30.98    unfolding One_nat_def by (rule gcd_1_left)
   30.99  
  30.100 -text {*
  30.101 +text \<open>
  30.102    \medskip Multiplication laws
  30.103 -*}
  30.104 +\<close>
  30.105  
  30.106  lemma gcd_mult_distrib2: "k * gcd m n = gcd (k * m) (k * n)"
  30.107 -    -- {* @{cite \<open>page 27\<close> davenport92} *}
  30.108 +    -- \<open>@{cite \<open>page 27\<close> davenport92}\<close>
  30.109    apply (induct m n rule: gcd_induct)
  30.110     apply simp
  30.111    apply (case_tac "k = 0")
  30.112 @@ -165,7 +165,7 @@
  30.113    done
  30.114  
  30.115  
  30.116 -text {* \medskip Addition laws *}
  30.117 +text \<open>\medskip Addition laws\<close>
  30.118  
  30.119  lemma gcd_add1 [simp, algebra]: "gcd (m + n) n = gcd m n"
  30.120    by (cases "n = 0") (auto simp add: gcd_non_0)
  30.121 @@ -190,9 +190,9 @@
  30.122  lemma gcd_dvd_prod: "gcd m n dvd m * n" 
  30.123    using mult_dvd_mono [of 1] by auto
  30.124  
  30.125 -text {*
  30.126 +text \<open>
  30.127    \medskip Division by gcd yields rrelatively primes.
  30.128 -*}
  30.129 +\<close>
  30.130  
  30.131  lemma div_gcd_relprime:
  30.132    assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
  30.133 @@ -313,7 +313,7 @@
  30.134  done
  30.135  
  30.136  
  30.137 -text {* We can get a stronger version with a nonzeroness assumption. *}
  30.138 +text \<open>We can get a stronger version with a nonzeroness assumption.\<close>
  30.139  lemma divides_le: "m dvd n ==> m <= n \<or> n = (0::nat)" by (auto simp add: dvd_def)
  30.140  
  30.141  lemma bezout_add_strong: assumes nz: "a \<noteq> (0::nat)"
  30.142 @@ -449,7 +449,7 @@
  30.143  qed
  30.144  
  30.145  
  30.146 -subsection {* LCM defined by GCD *}
  30.147 +subsection \<open>LCM defined by GCD\<close>
  30.148  
  30.149  
  30.150  definition
  30.151 @@ -562,7 +562,7 @@
  30.152    done
  30.153  
  30.154  
  30.155 -subsection {* GCD and LCM on integers *}
  30.156 +subsection \<open>GCD and LCM on integers\<close>
  30.157  
  30.158  definition
  30.159    zgcd :: "int \<Rightarrow> int \<Rightarrow> int" where
  30.160 @@ -595,7 +595,7 @@
  30.161  proof -
  30.162    assume "int (gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>)) = 1" "i dvd k * j"
  30.163    then have g: "gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>) = 1" by simp
  30.164 -  from `i dvd k * j` obtain h where h: "k*j = i*h" unfolding dvd_def by blast
  30.165 +  from \<open>i dvd k * j\<close> obtain h where h: "k*j = i*h" unfolding dvd_def by blast
  30.166    have th: "nat \<bar>i\<bar> dvd nat \<bar>k\<bar> * nat \<bar>j\<bar>"
  30.167      unfolding dvd_def
  30.168      by (rule_tac x= "nat \<bar>h\<bar>" in exI, simp add: h nat_abs_mult_distrib [symmetric])
  30.169 @@ -620,7 +620,7 @@
  30.170    let ?k' = "nat \<bar>k\<bar>"
  30.171    let ?m' = "nat \<bar>m\<bar>"
  30.172    let ?n' = "nat \<bar>n\<bar>"
  30.173 -  from `k dvd m` and `k dvd n` have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
  30.174 +  from \<open>k dvd m\<close> and \<open>k dvd n\<close> have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
  30.175      unfolding zdvd_int by (simp_all only: int_nat_abs abs_dvd_iff dvd_abs_iff)
  30.176    from gcd_greatest [OF dvd'] have "int (nat \<bar>k\<bar>) dvd zgcd m n"
  30.177      unfolding zgcd_def by (simp only: zdvd_int)
  30.178 @@ -696,7 +696,7 @@
  30.179    done
  30.180  
  30.181  lemmas zgcd_ac = zgcd_assoc zgcd_commute zgcd_left_commute
  30.182 -  -- {* addition is an AC-operator *}
  30.183 +  -- \<open>addition is an AC-operator\<close>
  30.184  
  30.185  lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd m n = zgcd (k * m) (k * n)"
  30.186    by (simp del: minus_mult_right [symmetric]
  30.187 @@ -728,7 +728,7 @@
  30.188  lemma dvd_imp_dvd_zlcm1:
  30.189    assumes "k dvd i" shows "k dvd (zlcm i j)"
  30.190  proof -
  30.191 -  have "nat(abs k) dvd nat(abs i)" using `k dvd i`
  30.192 +  have "nat(abs k) dvd nat(abs i)" using \<open>k dvd i\<close>
  30.193      by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
  30.194    thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
  30.195  qed
  30.196 @@ -736,7 +736,7 @@
  30.197  lemma dvd_imp_dvd_zlcm2:
  30.198    assumes "k dvd j" shows "k dvd (zlcm i j)"
  30.199  proof -
  30.200 -  have "nat(abs k) dvd nat(abs j)" using `k dvd j`
  30.201 +  have "nat(abs k) dvd nat(abs j)" using \<open>k dvd j\<close>
  30.202      by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
  30.203    thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
  30.204  qed
    31.1 --- a/src/HOL/Old_Number_Theory/Pocklington.thy	Sat Oct 10 16:21:34 2015 +0200
    31.2 +++ b/src/HOL/Old_Number_Theory/Pocklington.thy	Sat Oct 10 16:26:23 2015 +0200
    31.3 @@ -2,7 +2,7 @@
    31.4      Author:     Amine Chaieb
    31.5  *)
    31.6  
    31.7 -section {* Pocklington's Theorem for Primes *}
    31.8 +section \<open>Pocklington's Theorem for Primes\<close>
    31.9  
   31.10  theory Pocklington
   31.11  imports Primes
    32.1 --- a/src/HOL/Old_Number_Theory/Primes.thy	Sat Oct 10 16:21:34 2015 +0200
    32.2 +++ b/src/HOL/Old_Number_Theory/Primes.thy	Sat Oct 10 16:26:23 2015 +0200
    32.3 @@ -3,7 +3,7 @@
    32.4      Copyright   1996  University of Cambridge
    32.5  *)
    32.6  
    32.7 -section {* Primality on nat *}
    32.8 +section \<open>Primality on nat\<close>
    32.9  
   32.10  theory Primes
   32.11  imports Complex_Main Legacy_GCD
   32.12 @@ -27,11 +27,11 @@
   32.13    apply (metis gcd_dvd1 gcd_dvd2)
   32.14    done
   32.15  
   32.16 -text {*
   32.17 +text \<open>
   32.18    This theorem leads immediately to a proof of the uniqueness of
   32.19    factorization.  If @{term p} divides a product of primes then it is
   32.20    one of those primes.
   32.21 -*}
   32.22 +\<close>
   32.23  
   32.24  lemma prime_dvd_mult: "prime p ==> p dvd m * n ==> p dvd m \<or> p dvd n"
   32.25    by (blast intro: relprime_dvd_mult prime_imp_relprime)
   32.26 @@ -92,7 +92,7 @@
   32.27    ultimately show ?thesis by blast  
   32.28  qed
   32.29  
   32.30 -text {* Elementary theory of divisibility *}
   32.31 +text \<open>Elementary theory of divisibility\<close>
   32.32  lemma divides_ge: "(a::nat) dvd b \<Longrightarrow> b = 0 \<or> a \<le> b" unfolding dvd_def by auto
   32.33  lemma divides_antisym: "(x::nat) dvd y \<and> y dvd x \<longleftrightarrow> x = y"
   32.34    using dvd_antisym[of x y] by auto
   32.35 @@ -176,7 +176,7 @@
   32.36  lemma divides_rexp: 
   32.37    "x dvd y \<Longrightarrow> (x::nat) dvd (y^(Suc n))" by (simp add: dvd_mult2[of x y])
   32.38  
   32.39 -text {* Coprimality *}
   32.40 +text \<open>Coprimality\<close>
   32.41  
   32.42  lemma coprime: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   32.43  using gcd_unique[of 1 a b, simplified] by (auto simp add: coprime_def)
   32.44 @@ -379,7 +379,7 @@
   32.45  qed
   32.46  
   32.47  
   32.48 -text {* A binary form of the Chinese Remainder Theorem. *}
   32.49 +text \<open>A binary form of the Chinese Remainder Theorem.\<close>
   32.50  
   32.51  lemma chinese_remainder: assumes ab: "coprime a b" and a:"a \<noteq> 0" and b:"b \<noteq> 0"
   32.52    shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b"
   32.53 @@ -397,9 +397,9 @@
   32.54    thus ?thesis by blast
   32.55  qed
   32.56  
   32.57 -text {* Primality *}
   32.58 +text \<open>Primality\<close>
   32.59  
   32.60 -text {* A few useful theorems about primes *}
   32.61 +text \<open>A few useful theorems about primes\<close>
   32.62  
   32.63  lemma prime_0[simp]: "~prime 0" by (simp add: prime_def)
   32.64  lemma prime_1[simp]: "~ prime 1"  by (simp add: prime_def)
   32.65 @@ -591,7 +591,7 @@
   32.66  lemma prime_odd: "prime p \<Longrightarrow> p = 2 \<or> odd p" unfolding prime_def by auto
   32.67  
   32.68  
   32.69 -text {* One property of coprimality is easier to prove via prime factors. *}
   32.70 +text \<open>One property of coprimality is easier to prove via prime factors.\<close>
   32.71  
   32.72  lemma prime_divprod_pow: 
   32.73    assumes p: "prime p" and ab: "coprime a b" and pab: "p^n dvd a * b"
   32.74 @@ -714,7 +714,7 @@
   32.75  ultimately show ?ths by blast
   32.76  qed
   32.77  
   32.78 -text {* More useful lemmas. *}
   32.79 +text \<open>More useful lemmas.\<close>
   32.80  lemma prime_product: 
   32.81    assumes "prime (p * q)"
   32.82    shows "p = 1 \<or> q = 1"
   32.83 @@ -722,7 +722,7 @@
   32.84    from assms have 
   32.85      "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
   32.86      unfolding prime_def by auto
   32.87 -  from `1 < p * q` have "p \<noteq> 0" by (cases p) auto
   32.88 +  from \<open>1 < p * q\<close> have "p \<noteq> 0" by (cases p) auto
   32.89    then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
   32.90    have "p dvd p * q" by simp
   32.91    then have "p = 1 \<or> p = p * q" by (rule P)
    33.1 --- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sat Oct 10 16:21:34 2015 +0200
    33.2 +++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sat Oct 10 16:26:23 2015 +0200
    33.3 @@ -2,16 +2,16 @@
    33.4      Authors:    Jeremy Avigad, David Gray, and Adam Kramer
    33.5  *)
    33.6  
    33.7 -section {* The law of Quadratic reciprocity *}
    33.8 +section \<open>The law of Quadratic reciprocity\<close>
    33.9  
   33.10  theory Quadratic_Reciprocity
   33.11  imports Gauss
   33.12  begin
   33.13  
   33.14 -text {*
   33.15 +text \<open>
   33.16    Lemmas leading up to the proof of theorem 3.3 in Niven and
   33.17    Zuckerman's presentation.
   33.18 -*}
   33.19 +\<close>
   33.20  
   33.21  context GAUSS
   33.22  begin
   33.23 @@ -153,7 +153,7 @@
   33.24    done
   33.25  
   33.26  
   33.27 -subsection {* Stuff about S, S1 and S2 *}
   33.28 +subsection \<open>Stuff about S, S1 and S2\<close>
   33.29  
   33.30  locale QRTEMP =
   33.31    fixes p     :: "int"
    34.1 --- a/src/HOL/Old_Number_Theory/Residues.thy	Sat Oct 10 16:21:34 2015 +0200
    34.2 +++ b/src/HOL/Old_Number_Theory/Residues.thy	Sat Oct 10 16:26:23 2015 +0200
    34.3 @@ -2,15 +2,15 @@
    34.4      Authors:    Jeremy Avigad, David Gray, and Adam Kramer
    34.5  *)
    34.6  
    34.7 -section {* Residue Sets *}
    34.8 +section \<open>Residue Sets\<close>
    34.9  
   34.10  theory Residues
   34.11  imports Int2
   34.12  begin
   34.13  
   34.14 -text {*
   34.15 +text \<open>
   34.16    \medskip Define the residue of a set, the standard residue,
   34.17 -  quadratic residues, and prove some basic properties. *}
   34.18 +  quadratic residues, and prove some basic properties.\<close>
   34.19  
   34.20  definition ResSet :: "int => int set => bool"
   34.21    where "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))"
   34.22 @@ -33,7 +33,7 @@
   34.23    where "SRStar p = {x. (0 < x) & (x < p)}"
   34.24  
   34.25  
   34.26 -subsection {* Some useful properties of StandardRes *}
   34.27 +subsection \<open>Some useful properties of StandardRes\<close>
   34.28  
   34.29  lemma StandardRes_prop1: "[x = StandardRes m x] (mod m)"
   34.30    by (auto simp add: StandardRes_def zcong_zmod)
   34.31 @@ -61,7 +61,7 @@
   34.32    by (auto simp add: StandardRes_def zcong_eq_zdvd_prop dvd_def) 
   34.33  
   34.34  
   34.35 -subsection {* Relations between StandardRes, SRStar, and SR *}
   34.36 +subsection \<open>Relations between StandardRes, SRStar, and SR\<close>
   34.37  
   34.38  lemma SRStar_SR_prop: "x \<in> SRStar p ==> x \<in> SR p"
   34.39    by (auto simp add: SRStar_def SR_def)
   34.40 @@ -115,7 +115,7 @@
   34.41    by (auto simp add: SRStar_def bdd_int_set_l_l_finite)
   34.42  
   34.43  
   34.44 -subsection {* Properties relating ResSets with StandardRes *}
   34.45 +subsection \<open>Properties relating ResSets with StandardRes\<close>
   34.46  
   34.47  lemma aux: "x mod m = y mod m ==> [x = y] (mod m)"
   34.48    apply (subgoal_tac "x = y ==> [x = y](mod m)")
   34.49 @@ -158,7 +158,7 @@
   34.50    by (auto simp add: ResSet_def)
   34.51  
   34.52  
   34.53 -subsection {* Property for SRStar *}
   34.54 +subsection \<open>Property for SRStar\<close>
   34.55  
   34.56  lemma ResSet_SRStar_prop: "ResSet p (SRStar p)"
   34.57    by (auto simp add: SRStar_def ResSet_def zcong_zless_imp_eq)
    35.1 --- a/src/HOL/Old_Number_Theory/WilsonBij.thy	Sat Oct 10 16:21:34 2015 +0200
    35.2 +++ b/src/HOL/Old_Number_Theory/WilsonBij.thy	Sat Oct 10 16:26:23 2015 +0200
    35.3 @@ -3,20 +3,20 @@
    35.4      Copyright   2000  University of Cambridge
    35.5  *)
    35.6  
    35.7 -section {* Wilson's Theorem using a more abstract approach *}
    35.8 +section \<open>Wilson's Theorem using a more abstract approach\<close>
    35.9  
   35.10  theory WilsonBij
   35.11  imports BijectionRel IntFact
   35.12  begin
   35.13  
   35.14 -text {*
   35.15 +text \<open>
   35.16    Wilson's Theorem using a more ``abstract'' approach based on
   35.17    bijections between sets.  Does not use Fermat's Little Theorem
   35.18    (unlike Russinoff).
   35.19 -*}
   35.20 +\<close>
   35.21  
   35.22  
   35.23 -subsection {* Definitions and lemmas *}
   35.24 +subsection \<open>Definitions and lemmas\<close>
   35.25  
   35.26  definition reciR :: "int => int => int => bool"
   35.27    where "reciR p = (\<lambda>a b. zcong (a * b) 1 p \<and> 1 < a \<and> a < p - 1 \<and> 1 < b \<and> b < p - 1)"
   35.28 @@ -28,7 +28,7 @@
   35.29       else 0)"
   35.30  
   35.31  
   35.32 -text {* \medskip Inverse *}
   35.33 +text \<open>\medskip Inverse\<close>
   35.34  
   35.35  lemma inv_correct:
   35.36    "zprime p ==> 0 < a ==> a < p
   35.37 @@ -47,7 +47,7 @@
   35.38  
   35.39  lemma inv_not_0:
   35.40    "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> 0"
   35.41 -  -- {* same as @{text WilsonRuss} *}
   35.42 +  -- \<open>same as @{text WilsonRuss}\<close>
   35.43    apply safe
   35.44    apply (cut_tac a = a and p = p in inv_is_inv)
   35.45       apply (unfold zcong_def)
   35.46 @@ -56,7 +56,7 @@
   35.47  
   35.48  lemma inv_not_1:
   35.49    "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> 1"
   35.50 -  -- {* same as @{text WilsonRuss} *}
   35.51 +  -- \<open>same as @{text WilsonRuss}\<close>
   35.52    apply safe
   35.53    apply (cut_tac a = a and p = p in inv_is_inv)
   35.54       prefer 4
   35.55 @@ -67,7 +67,7 @@
   35.56    done
   35.57  
   35.58  lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
   35.59 -  -- {* same as @{text WilsonRuss} *}
   35.60 +  -- \<open>same as @{text WilsonRuss}\<close>
   35.61    apply (unfold zcong_def)
   35.62    apply (simp add: diff_diff_eq diff_diff_eq2 right_diff_distrib)
   35.63    apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
   35.64 @@ -81,7 +81,7 @@
   35.65  
   35.66  lemma inv_not_p_minus_1:
   35.67    "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> p - 1"
   35.68 -  -- {* same as @{text WilsonRuss} *}
   35.69 +  -- \<open>same as @{text WilsonRuss}\<close>
   35.70    apply safe
   35.71    apply (cut_tac a = a and p = p in inv_is_inv)
   35.72       apply auto
   35.73 @@ -91,10 +91,10 @@
   35.74         apply auto
   35.75    done
   35.76  
   35.77 -text {*
   35.78 +text \<open>
   35.79    Below is slightly different as we don't expand @{term [source] inv}
   35.80    but use ``@{text correct}'' theorems.
   35.81 -*}
   35.82 +\<close>
   35.83  
   35.84  lemma inv_g_1: "zprime p ==> 1 < a ==> a < p - 1 ==> 1 < inv p a"
   35.85    apply (subgoal_tac "inv p a \<noteq> 1")
   35.86 @@ -111,13 +111,13 @@
   35.87  
   35.88  lemma inv_less_p_minus_1:
   35.89    "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a < p - 1"
   35.90 -  -- {* ditto *}
   35.91 +  -- \<open>ditto\<close>
   35.92    apply (subst order_less_le)
   35.93    apply (simp add: inv_not_p_minus_1 inv_less)
   35.94    done
   35.95  
   35.96  
   35.97 -text {* \medskip Bijection *}
   35.98 +text \<open>\medskip Bijection\<close>
   35.99  
  35.100  lemma aux1: "1 < x ==> 0 \<le> (x::int)"
  35.101    apply auto
  35.102 @@ -139,9 +139,9 @@
  35.103    apply (unfold inj_on_def)
  35.104    apply auto
  35.105    apply (rule zcong_zless_imp_eq)
  35.106 -      apply (tactic {* stac @{context} (@{thm zcong_cancel} RS sym) 5 *})
  35.107 +      apply (tactic \<open>stac @{context} (@{thm zcong_cancel} RS sym) 5\<close>)
  35.108          apply (rule_tac [7] zcong_trans)
  35.109 -         apply (tactic {* stac @{context} @{thm zcong_sym} 8 *})
  35.110 +         apply (tactic \<open>stac @{context} @{thm zcong_sym} 8\<close>)
  35.111           apply (erule_tac [7] inv_is_inv)
  35.112            apply (tactic "asm_simp_tac @{context} 9")
  35.113            apply (erule_tac [9] inv_is_inv)
  35.114 @@ -192,15 +192,15 @@
  35.115    apply (unfold reciR_def uniqP_def)
  35.116    apply auto
  35.117     apply (rule zcong_zless_imp_eq)
  35.118 -       apply (tactic {* stac @{context} (@{thm zcong_cancel2} RS sym) 5 *})
  35.119 +       apply (tactic \<open>stac @{context} (@{thm zcong_cancel2} RS sym) 5\<close>)
  35.120           apply (rule_tac [7] zcong_trans)
  35.121 -          apply (tactic {* stac @{context} @{thm zcong_sym} 8 *})
  35.122 +          apply (tactic \<open>stac @{context} @{thm zcong_sym} 8\<close>)
  35.123            apply (rule_tac [6] zless_zprime_imp_zrelprime)
  35.124              apply auto
  35.125    apply (rule zcong_zless_imp_eq)
  35.126 -      apply (tactic {* stac @{context} (@{thm zcong_cancel} RS sym) 5 *})
  35.127 +      apply (tactic \<open>stac @{context} (@{thm zcong_cancel} RS sym) 5\<close>)
  35.128          apply (rule_tac [7] zcong_trans)
  35.129 -         apply (tactic {* stac @{context} @{thm zcong_sym} 8 *})
  35.130 +         apply (tactic \<open>stac @{context} @{thm zcong_sym} 8\<close>)
  35.131           apply (rule_tac [6] zless_zprime_imp_zrelprime)
  35.132             apply auto
  35.133    done
  35.134 @@ -220,7 +220,7 @@
  35.135    done
  35.136  
  35.137  
  35.138 -subsection {* Wilson *}
  35.139 +subsection \<open>Wilson\<close>
  35.140  
  35.141  lemma bijER_zcong_prod_1:
  35.142      "zprime p ==> A \<in> bijER (reciR p) ==> [\<Prod>A = 1] (mod p)"
    36.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Sat Oct 10 16:21:34 2015 +0200
    36.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Sat Oct 10 16:26:23 2015 +0200
    36.3 @@ -3,18 +3,18 @@
    36.4      Copyright   2000  University of Cambridge
    36.5  *)
    36.6  
    36.7 -section {* Wilson's Theorem according to Russinoff *}
    36.8 +section \<open>Wilson's Theorem according to Russinoff\<close>
    36.9  
   36.10  theory WilsonRuss
   36.11  imports EulerFermat
   36.12  begin
   36.13  
   36.14 -text {*
   36.15 +text \<open>
   36.16    Wilson's Theorem following quite closely Russinoff's approach
   36.17    using Boyer-Moore (using finite sets instead of lists, though).
   36.18 -*}
   36.19 +\<close>
   36.20  
   36.21 -subsection {* Definitions and lemmas *}
   36.22 +subsection \<open>Definitions and lemmas\<close>
   36.23  
   36.24  definition inv :: "int => int => int"
   36.25    where "inv p a = (a^(nat (p - 2))) mod p"
   36.26 @@ -26,7 +26,7 @@
   36.27        in (if a \<in> ws then ws else insert a (insert (inv p a) ws)) else {})"
   36.28  
   36.29  
   36.30 -text {* \medskip @{term [source] inv} *}
   36.31 +text \<open>\medskip @{term [source] inv}\<close>
   36.32  
   36.33  lemma inv_is_inv_aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)"
   36.34    by (subst int_int_eq [symmetric]) auto
   36.35 @@ -149,7 +149,7 @@
   36.36    done
   36.37  
   36.38  
   36.39 -text {* \medskip @{term wset} *}
   36.40 +text \<open>\medskip @{term wset}\<close>
   36.41  
   36.42  declare wset.simps [simp del]
   36.43  
   36.44 @@ -252,7 +252,7 @@
   36.45     apply (subst wset.simps)
   36.46     apply (auto, unfold Let_def, auto)
   36.47    apply (subst setprod.insert)
   36.48 -    apply (tactic {* stac @{context} @{thm setprod.insert} 3 *})
   36.49 +    apply (tactic \<open>stac @{context} @{thm setprod.insert} 3\<close>)
   36.50        apply (subgoal_tac [5]
   36.51          "zcong (a * inv p a * (\<Prod>x\<in>wset (a - 1) p. x)) (1 * 1) p")
   36.52         prefer 5
   36.53 @@ -281,7 +281,7 @@
   36.54    done
   36.55  
   36.56  
   36.57 -subsection {* Wilson *}
   36.58 +subsection \<open>Wilson\<close>
   36.59  
   36.60  lemma prime_g_5: "zprime p \<Longrightarrow> p \<noteq> 2 \<Longrightarrow> p \<noteq> 3 ==> 5 \<le> p"
   36.61    apply (unfold zprime_def dvd_def)