# HG changeset patch
# User wenzelm
# Date 1444487183 -7200
# Node ID efac889fccbcfa34f01aa605a92635382fe1d87b
# Parent  ddca85598c659453611448b647abde93fe767713
isabelle update_cartouches;

diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/AbelCoset.thy
--- a/src/HOL/Algebra/AbelCoset.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/AbelCoset.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -6,12 +6,12 @@
 imports Coset Ring
 begin
 
-subsection {* More Lifting from Groups to Abelian Groups *}
+subsection \<open>More Lifting from Groups to Abelian Groups\<close>
 
-subsubsection {* Definitions *}
+subsubsection \<open>Definitions\<close>
 
-text {* Hiding @{text "<+>"} from @{theory Sum_Type} until I come
-  up with better syntax here *}
+text \<open>Hiding @{text "<+>"} from @{theory Sum_Type} until I come
+  up with better syntax here\<close>
 
 no_notation Sum_Type.Plus (infixr "<+>" 65)
 
@@ -41,12 +41,12 @@
 
 definition
   A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "A'_Mod" 65)
-    --{*Actually defined for groups rather than monoids*}
+    --\<open>Actually defined for groups rather than monoids\<close>
   where "A_FactGroup G H = FactGroup \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
 
 definition
   a_kernel :: "('a, 'm) ring_scheme \<Rightarrow> ('b, 'n) ring_scheme \<Rightarrow>  ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
-    --{*the kernel of a homomorphism (additive)*}
+    --\<open>the kernel of a homomorphism (additive)\<close>
   where "a_kernel G H h =
     kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
       \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
@@ -103,7 +103,7 @@
 by (fold a_inv_def)
 
 
-subsubsection {* Cosets *}
+subsubsection \<open>Cosets\<close>
 
 lemma (in abelian_group) a_coset_add_assoc:
      "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
@@ -163,7 +163,7 @@
 by (rule group.rcosetsI [OF a_group,
     folded a_r_coset_def A_RCOSETS_def, simplified monoid_record_simps])
 
-text{*Really needed?*}
+text\<open>Really needed?\<close>
 lemma (in abelian_group) a_transpose_inv:
      "[| x \<oplus> y = z;  x \<in> carrier G;  y \<in> carrier G;  z \<in> carrier G |]
       ==> (\<ominus> x) \<oplus> z = y"
@@ -179,7 +179,7 @@
 *)
 
 
-subsubsection {* Subgroups *}
+subsubsection \<open>Subgroups\<close>
 
 locale additive_subgroup =
   fixes H and G (structure)
@@ -216,9 +216,9 @@
     folded a_inv_def, simplified monoid_record_simps])
 
 
-subsubsection {* Additive subgroups are normal *}
+subsubsection \<open>Additive subgroups are normal\<close>
 
-text {* Every subgroup of an @{text "abelian_group"} is normal *}
+text \<open>Every subgroup of an @{text "abelian_group"} is normal\<close>
 
 locale abelian_subgroup = additive_subgroup + abelian_group G +
   assumes a_normal: "normal H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
@@ -287,7 +287,7 @@
 by (rule normal.inv_op_closed2 [OF a_normal,
     folded a_inv_def, simplified monoid_record_simps])
 
-text{*Alternative characterization of normal subgroups*}
+text\<open>Alternative characterization of normal subgroups\<close>
 lemma (in abelian_group) a_normal_inv_iff:
      "(N \<lhd> \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>) = 
       (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))"
@@ -378,12 +378,12 @@
 
 lemma (in abelian_subgroup) rcosets_add_eq:
   "M \<in> a_rcosets H \<Longrightarrow> H <+> M = M"
-  -- {* generalizes @{text subgroup_mult_id} *}
+  -- \<open>generalizes @{text subgroup_mult_id}\<close>
 by (rule normal.rcosets_mult_eq [OF a_normal,
     folded set_add_def A_RCOSETS_def, simplified monoid_record_simps])
 
 
-subsubsection {* Congruence Relation *}
+subsubsection \<open>Congruence Relation\<close>
 
 lemma (in abelian_subgroup) a_equiv_rcong:
    shows "equiv (carrier G) (racong H)"
@@ -444,7 +444,7 @@
     (fast intro!: additive_subgroup.a_subgroup)+
 
 
-subsubsection {* Factorization *}
+subsubsection \<open>Factorization\<close>
 
 lemmas A_FactGroup_defs = A_FactGroup_def FactGroup_def
 
@@ -486,8 +486,8 @@
 by (rule normal.factorgroup_is_group [OF a_normal,
     folded A_FactGroup_def, simplified monoid_record_simps])
 
-text {* Since the Factorization is based on an \emph{abelian} subgroup, is results in 
-        a commutative group *}
+text \<open>Since the Factorization is based on an \emph{abelian} subgroup, is results in 
+        a commutative group\<close>
 theorem (in abelian_subgroup) a_factorgroup_is_comm_group:
   "comm_group (G A_Mod H)"
 apply (intro comm_group.intro comm_monoid.intro) prefer 3
@@ -506,21 +506,21 @@
 by (rule normal.inv_FactGroup [OF a_normal,
     folded A_FactGroup_def A_SET_INV_def, simplified monoid_record_simps])
 
-text{*The coset map is a homomorphism from @{term G} to the quotient group
-  @{term "G Mod H"}*}
+text\<open>The coset map is a homomorphism from @{term G} to the quotient group
+  @{term "G Mod H"}\<close>
 lemma (in abelian_subgroup) a_r_coset_hom_A_Mod:
   "(\<lambda>a. H +> a) \<in> hom \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> (G A_Mod H)"
 by (rule normal.r_coset_hom_Mod [OF a_normal,
     folded A_FactGroup_def a_r_coset_def, simplified monoid_record_simps])
 
-text {* The isomorphism theorems have been omitted from lifting, at
-  least for now *}
+text \<open>The isomorphism theorems have been omitted from lifting, at
+  least for now\<close>
 
 
-subsubsection{*The First Isomorphism Theorem*}
+subsubsection\<open>The First Isomorphism Theorem\<close>
 
-text{*The quotient by the kernel of a homomorphism is isomorphic to the 
-  range of that homomorphism.*}
+text\<open>The quotient by the kernel of a homomorphism is isomorphic to the 
+  range of that homomorphism.\<close>
 
 lemmas a_kernel_defs =
   a_kernel_def kernel_def
@@ -530,7 +530,7 @@
 by (rule a_kernel_def[unfolded kernel_def, simplified ring_record_simps])
 
 
-subsubsection {* Homomorphisms *}
+subsubsection \<open>Homomorphisms\<close>
 
 lemma abelian_group_homI:
   assumes "abelian_group G"
@@ -591,7 +591,7 @@
        folded a_kernel_def, simplified ring_record_simps])
 done
 
-text{*The kernel of a homomorphism is an abelian subgroup*}
+text\<open>The kernel of a homomorphism is an abelian subgroup\<close>
 lemma (in abelian_group_hom) abelian_subgroup_a_kernel:
   "abelian_subgroup (a_kernel G H h) G"
 apply (rule abelian_subgroupI)
@@ -623,16 +623,16 @@
 by (rule group_hom.FactGroup_inj_on[OF a_group_hom,
     folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
 
-text{*If the homomorphism @{term h} is onto @{term H}, then so is the
-homomorphism from the quotient group*}
+text\<open>If the homomorphism @{term h} is onto @{term H}, then so is the
+homomorphism from the quotient group\<close>
 lemma (in abelian_group_hom) A_FactGroup_onto:
   assumes h: "h ` carrier G = carrier H"
   shows "(\<lambda>X. the_elem (h ` X)) ` carrier (G A_Mod a_kernel G H h) = carrier H"
 by (rule group_hom.FactGroup_onto[OF a_group_hom,
     folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule h)
 
-text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
- quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
+text\<open>If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
+ quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.\<close>
 theorem (in abelian_group_hom) A_FactGroup_iso:
   "h ` carrier G = carrier H
    \<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> (G A_Mod (a_kernel G H h)) \<cong>
@@ -641,9 +641,9 @@
     folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
 
 
-subsubsection {* Cosets *}
+subsubsection \<open>Cosets\<close>
 
-text {* Not eveything from \texttt{CosetExt.thy} is lifted here. *}
+text \<open>Not eveything from \texttt{CosetExt.thy} is lifted here.\<close>
 
 lemma (in additive_subgroup) a_Hcarr [simp]:
   assumes hH: "h \<in> H"
@@ -725,7 +725,7 @@
     folded A_RCOSETS_def, simplified monoid_record_simps])
 
 
-subsubsection {* Addition of Subgroups *}
+subsubsection \<open>Addition of Subgroups\<close>
 
 lemma (in abelian_monoid) set_add_closed:
   assumes Acarr: "A \<subseteq> carrier G"
diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/Bij.thy
--- a/src/HOL/Algebra/Bij.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/Bij.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -6,11 +6,11 @@
 imports Group
 begin
 
-section {* Bijections of a Set, Permutation and Automorphism Groups *}
+section \<open>Bijections of a Set, Permutation and Automorphism Groups\<close>
 
 definition
   Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set"
-    --{*Only extensional functions, since otherwise we get too many.*}
+    --\<open>Only extensional functions, since otherwise we get too many.\<close>
    where "Bij S = extensional S \<inter> {f. bij_betw f S S}"
 
 definition
@@ -30,7 +30,7 @@
   by (auto simp add: Bij_def bij_betw_imp_funcset)
 
 
-subsection {*Bijections Form a Group *}
+subsection \<open>Bijections Form a Group\<close>
 
 lemma restrict_inv_into_Bij: "f \<in> Bij S \<Longrightarrow> (\<lambda>x \<in> S. (inv_into S f) x) \<in> Bij S"
   by (simp add: Bij_def bij_betw_inv_into)
@@ -57,7 +57,7 @@
 done
 
 
-subsection{*Automorphisms Form a Group*}
+subsection\<open>Automorphisms Form a Group\<close>
 
 lemma Bij_inv_into_mem: "\<lbrakk> f \<in> Bij S;  x \<in> S\<rbrakk> \<Longrightarrow> inv_into S f x \<in> S"
 by (simp add: Bij_def bij_betw_def inv_into_into)
diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/Congruence.thy
--- a/src/HOL/Algebra/Congruence.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/Congruence.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -7,15 +7,15 @@
 imports Main
 begin
 
-section {* Objects *}
+section \<open>Objects\<close>
 
-subsection {* Structure with Carrier Set. *}
+subsection \<open>Structure with Carrier Set.\<close>
 
 record 'a partial_object =
   carrier :: "'a set"
 
 
-subsection {* Structure with Carrier and Equivalence Relation @{text eq} *}
+subsection \<open>Structure with Carrier and Equivalence Relation @{text eq}\<close>
 
 record 'a eq_object = "'a partial_object" +
   eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".=\<index>" 50)
diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/Coset.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -8,7 +8,7 @@
 imports Group
 begin
 
-section {*Cosets and Quotient Groups*}
+section \<open>Cosets and Quotient Groups\<close>
 
 definition
   r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "#>\<index>" 60)
@@ -39,7 +39,7 @@
   "H \<lhd> G \<equiv> normal H G"
 
 
-subsection {*Basic Properties of Cosets*}
+subsection \<open>Basic Properties of Cosets\<close>
 
 lemma (in group) coset_mult_assoc:
      "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
@@ -85,7 +85,7 @@
 
 lemma (in group) coset_join2:
      "\<lbrakk>x \<in> carrier G;  subgroup H G;  x\<in>H\<rbrakk> \<Longrightarrow> H #> x = H"
-  --{*Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.*}
+  --\<open>Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.\<close>
 by (force simp add: subgroup.m_closed r_coset_def solve_equation)
 
 lemma (in monoid) r_coset_subset_G:
@@ -100,7 +100,7 @@
      "\<lbrakk>H \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow> H #> x \<in> rcosets H"
 by (auto simp add: RCOSETS_def)
 
-text{*Really needed?*}
+text\<open>Really needed?\<close>
 lemma (in group) transpose_inv:
      "[| x \<otimes> y = z;  x \<in> carrier G;  y \<in> carrier G;  z \<in> carrier G |]
       ==> (inv x) \<otimes> z = y"
@@ -112,7 +112,7 @@
                     subgroup.one_closed)
 done
 
-text (in group) {* Opposite of @{thm [source] "repr_independence"} *}
+text (in group) \<open>Opposite of @{thm [source] "repr_independence"}\<close>
 lemma (in group) repr_independenceD:
   assumes "subgroup H G"
   assumes ycarr: "y \<in> carrier G"
@@ -127,7 +127,7 @@
   done
 qed
 
-text {* Elements of a right coset are in the carrier *}
+text \<open>Elements of a right coset are in the carrier\<close>
 lemma (in subgroup) elemrcos_carrier:
   assumes "group G"
   assumes acarr: "a \<in> carrier G"
@@ -171,7 +171,7 @@
   qed
 qed
 
-text {* Step one for lemma @{text "rcos_module"} *}
+text \<open>Step one for lemma @{text "rcos_module"}\<close>
 lemma (in subgroup) rcos_module_imp:
   assumes "group G"
   assumes xcarr: "x \<in> carrier G"
@@ -211,7 +211,7 @@
       show "x' \<otimes> (inv x) \<in> H" by simp
 qed
 
-text {* Step two for lemma @{text "rcos_module"} *}
+text \<open>Step two for lemma @{text "rcos_module"}\<close>
 lemma (in subgroup) rcos_module_rev:
   assumes "group G"
   assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
@@ -243,7 +243,7 @@
       by fast
 qed
 
-text {* Module property of right cosets *}
+text \<open>Module property of right cosets\<close>
 lemma (in subgroup) rcos_module:
   assumes "group G"
   assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
@@ -262,7 +262,7 @@
   qed
 qed
 
-text {* Right cosets are subsets of the carrier. *} 
+text \<open>Right cosets are subsets of the carrier.\<close> 
 lemma (in subgroup) rcosets_carrier:
   assumes "group G"
   assumes XH: "X \<in> rcosets H"
@@ -283,7 +283,7 @@
       by (rule r_coset_subset_G)
 qed
 
-text {* Multiplication of general subsets *}
+text \<open>Multiplication of general subsets\<close>
 lemma (in monoid) set_mult_closed:
   assumes Acarr: "A \<subseteq> carrier G"
       and Bcarr: "B \<subseteq> carrier G"
@@ -381,7 +381,7 @@
 qed
 
 
-subsection {* Normal subgroups *}
+subsection \<open>Normal subgroups\<close>
 
 lemma normal_imp_subgroup: "H \<lhd> G \<Longrightarrow> subgroup H G"
   by (simp add: normal_def subgroup_def)
@@ -407,7 +407,7 @@
 apply (blast intro: inv_op_closed1) 
 done
 
-text{*Alternative characterization of normal subgroups*}
+text\<open>Alternative characterization of normal subgroups\<close>
 lemma (in group) normal_inv_iff:
      "(N \<lhd> G) = 
       (subgroup N G & (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<otimes> h \<otimes> (inv x) \<in> N))"
@@ -456,7 +456,7 @@
 qed
 
 
-subsection{*More Properties of Cosets*}
+subsection\<open>More Properties of Cosets\<close>
 
 lemma (in group) lcos_m_assoc:
      "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
@@ -524,7 +524,7 @@
 done
 
 
-subsubsection {* Set of Inverses of an @{text r_coset}. *}
+subsubsection \<open>Set of Inverses of an @{text r_coset}.\<close>
 
 lemma (in normal) rcos_inv:
   assumes x:     "x \<in> carrier G"
@@ -549,7 +549,7 @@
 qed
 
 
-subsubsection {*Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.*}
+subsubsection \<open>Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.\<close>
 
 lemma (in group) setmult_rcos_assoc:
      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
@@ -584,12 +584,12 @@
 by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
 
 lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
-  -- {* generalizes @{text subgroup_mult_id} *}
+  -- \<open>generalizes @{text subgroup_mult_id}\<close>
   by (auto simp add: RCOSETS_def subset
         setmult_rcos_assoc subgroup_mult_id normal.axioms normal_axioms)
 
 
-subsubsection{*An Equivalence Relation*}
+subsubsection\<open>An Equivalence Relation\<close>
 
 definition
   r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set"  ("rcong\<index> _")
@@ -628,9 +628,9 @@
   qed
 qed
 
-text{*Equivalence classes of @{text rcong} correspond to left cosets.
+text\<open>Equivalence classes of @{text rcong} correspond to left cosets.
   Was there a mistake in the definitions? I'd have expected them to
-  correspond to right cosets.*}
+  correspond to right cosets.\<close>
 
 (* CB: This is correct, but subtle.
    We call H #> a the right coset of a relative to H.  According to
@@ -652,7 +652,7 @@
 qed
 
 
-subsubsection{*Two Distinct Right Cosets are Disjoint*}
+subsubsection\<open>Two Distinct Right Cosets are Disjoint\<close>
 
 lemma (in group) rcos_equation:
   assumes "subgroup H G"
@@ -679,9 +679,9 @@
 qed
 
 
-subsection {* Further lemmas for @{text "r_congruent"} *}
+subsection \<open>Further lemmas for @{text "r_congruent"}\<close>
 
-text {* The relation is a congruence *}
+text \<open>The relation is a congruence\<close>
 
 lemma (in normal) congruent_rcong:
   shows "congruent2 (rcong H) (rcong H) (\<lambda>a b. a \<otimes> b <# H)"
@@ -753,7 +753,7 @@
 qed
 
 
-subsection {*Order of a Group and Lagrange's Theorem*}
+subsection \<open>Order of a Group and Lagrange's Theorem\<close>
 
 definition
   order :: "('a, 'b) monoid_scheme \<Rightarrow> nat"
@@ -777,7 +777,7 @@
 apply (simp add: r_coset_subset_G [THEN finite_subset])
 done
 
-text{*The next two lemmas support the proof of @{text card_cosets_equal}.*}
+text\<open>The next two lemmas support the proof of @{text card_cosets_equal}.\<close>
 lemma (in group) inj_on_f:
     "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
 apply (rule inj_onI)
@@ -799,7 +799,7 @@
     apply (force simp add: m_assoc subsetD r_coset_def)
    apply (rule inj_on_g, assumption+)
   apply (force simp add: m_assoc subsetD r_coset_def)
- txt{*The sets @{term "H #> a"} and @{term "H"} are finite.*}
+ txt\<open>The sets @{term "H #> a"} and @{term "H"} are finite.\<close>
  apply (simp add: r_coset_subset_G [THEN finite_subset])
 apply (blast intro: finite_subset)
 done
@@ -824,11 +824,11 @@
 done
 
 
-subsection {*Quotient Groups: Factorization of a Group*}
+subsection \<open>Quotient Groups: Factorization of a Group\<close>
 
 definition
   FactGroup :: "[('a,'b) monoid_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "Mod" 65)
-    --{*Actually defined for groups rather than monoids*}
+    --\<open>Actually defined for groups rather than monoids\<close>
    where "FactGroup G H = \<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
 
 lemma (in normal) setmult_closed:
@@ -880,21 +880,21 @@
 apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
 done
 
-text{*The coset map is a homomorphism from @{term G} to the quotient group
-  @{term "G Mod H"}*}
+text\<open>The coset map is a homomorphism from @{term G} to the quotient group
+  @{term "G Mod H"}\<close>
 lemma (in normal) r_coset_hom_Mod:
   "(\<lambda>a. H #> a) \<in> hom G (G Mod H)"
   by (auto simp add: FactGroup_def RCOSETS_def Pi_def hom_def rcos_sum)
 
  
-subsection{*The First Isomorphism Theorem*}
+subsection\<open>The First Isomorphism Theorem\<close>
 
-text{*The quotient by the kernel of a homomorphism is isomorphic to the 
-  range of that homomorphism.*}
+text\<open>The quotient by the kernel of a homomorphism is isomorphic to the 
+  range of that homomorphism.\<close>
 
 definition
   kernel :: "('a, 'm) monoid_scheme \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow>  ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
-    --{*the kernel of a homomorphism*}
+    --\<open>the kernel of a homomorphism\<close>
   where "kernel G H h = {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}"
 
 lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
@@ -902,7 +902,7 @@
 apply (auto simp add: kernel_def group.intro is_group) 
 done
 
-text{*The kernel of a homomorphism is a normal subgroup*}
+text\<open>The kernel of a homomorphism is a normal subgroup\<close>
 lemma (in group_hom) normal_kernel: "(kernel G H h) \<lhd> G"
 apply (simp add: G.normal_inv_iff subgroup_kernel)
 apply (simp add: kernel_def)
@@ -957,7 +957,7 @@
 qed
 
 
-text{*Lemma for the following injectivity result*}
+text\<open>Lemma for the following injectivity result\<close>
 lemma (in group_hom) FactGroup_subset:
      "\<lbrakk>g \<in> carrier G; g' \<in> carrier G; h g = h g'\<rbrakk>
       \<Longrightarrow>  kernel G H h #> g \<subseteq> kernel G H h #> g'"
@@ -986,8 +986,8 @@
   show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX) 
 qed
 
-text{*If the homomorphism @{term h} is onto @{term H}, then so is the
-homomorphism from the quotient group*}
+text\<open>If the homomorphism @{term h} is onto @{term H}, then so is the
+homomorphism from the quotient group\<close>
 lemma (in group_hom) FactGroup_onto:
   assumes h: "h ` carrier G = carrier H"
   shows "(\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
@@ -1008,8 +1008,8 @@
 qed
 
 
-text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
- quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
+text\<open>If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
+ quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.\<close>
 theorem (in group_hom) FactGroup_iso:
   "h ` carrier G = carrier H
    \<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -3,15 +3,15 @@
     Author:     Stephan Hohe
 *)
 
-section {* Divisibility in monoids and rings *}
+section \<open>Divisibility in monoids and rings\<close>
 
 theory Divisibility
 imports "~~/src/HOL/Library/Permutation" Coset Group
 begin
 
-section {* Factorial Monoids *}
-
-subsection {* Monoids with Cancellation Law *}
+section \<open>Factorial Monoids\<close>
+
+subsection \<open>Monoids with Cancellation Law\<close>
 
 locale monoid_cancel = monoid +
   assumes l_cancel: 
@@ -57,7 +57,7 @@
   ..
 
 
-subsection {* Products of Units in Monoids *}
+subsection \<open>Products of Units in Monoids\<close>
 
 lemma (in monoid) Units_m_closed[simp, intro]:
   assumes h1unit: "h1 \<in> Units G" and h2unit: "h2 \<in> Units G"
@@ -144,9 +144,9 @@
 qed
 
 
-subsection {* Divisibility and Association *}
-
-subsubsection {* Function definitions *}
+subsection \<open>Divisibility and Association\<close>
+
+subsubsection \<open>Function definitions\<close>
 
 definition
   factor :: "[_, 'a, 'a] \<Rightarrow> bool" (infix "divides\<index>" 65)
@@ -174,7 +174,7 @@
     (\<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)"
 
 
-subsubsection {* Divisibility *}
+subsubsection \<open>Divisibility\<close>
 
 lemma dividesI:
   fixes G (structure)
@@ -309,7 +309,7 @@
 by (fast dest: divides_unit intro: unit_divides)
 
 
-subsubsection {* Association *}
+subsubsection \<open>Association\<close>
 
 lemma associatedI:
   fixes G (structure)
@@ -449,7 +449,7 @@
   done
 
 
-subsubsection {* Division and associativity *}
+subsubsection \<open>Division and associativity\<close>
 
 lemma divides_antisym:
   fixes G (structure)
@@ -497,7 +497,7 @@
   done
 
     
-subsubsection {* Multiplication and associativity *}
+subsubsection \<open>Multiplication and associativity\<close>
 
 lemma (in monoid_cancel) mult_cong_r:
   assumes "b \<sim> b'"
@@ -545,7 +545,7 @@
 done
 
 
-subsubsection {* Units *}
+subsubsection \<open>Units\<close>
 
 lemma (in monoid_cancel) assoc_unit_l [trans]:
   assumes asc: "a \<sim> b" and bunit: "b \<in> Units G"
@@ -604,7 +604,7 @@
 done
 
 
-subsubsection {* Proper factors *}
+subsubsection \<open>Proper factors\<close>
 
 lemma properfactorI:
   fixes G (structure)
@@ -785,9 +785,9 @@
 by (intro properfactor_trans2[OF ab] divides_prod_l, simp+)
 
 
-subsection {* Irreducible Elements and Primes *}
-
-subsubsection {* Irreducible elements *}
+subsection \<open>Irreducible Elements and Primes\<close>
+
+subsubsection \<open>Irreducible elements\<close>
 
 lemma irreducibleI:
   fixes G (structure)
@@ -903,7 +903,7 @@
 qed
 
 
-subsubsection {* Prime elements *}
+subsubsection \<open>Prime elements\<close>
 
 lemma primeI:
   fixes G (structure)
@@ -943,9 +943,9 @@
 apply (metis assms(2) assms(3) assms(4) associated_sym divides_cong_l m_closed)
 done
 
-subsection {* Factorization and Factorial Monoids *}
-
-subsubsection {* Function definitions *}
+subsection \<open>Factorization and Factorial Monoids\<close>
+
+subsubsection \<open>Function definitions\<close>
 
 definition
   factors :: "[_, 'a list, 'a] \<Rightarrow> bool"
@@ -972,9 +972,9 @@
             set fs \<subseteq> carrier G; set fs' \<subseteq> carrier G\<rbrakk> \<Longrightarrow> essentially_equal G fs fs'"
 
 
-subsubsection {* Comparing lists of elements *}
-
-text {* Association on lists *}
+subsubsection \<open>Comparing lists of elements\<close>
+
+text \<open>Association on lists\<close>
 
 lemma (in monoid) listassoc_refl [simp, intro]:
   assumes "set as \<subseteq> carrier G"
@@ -1019,7 +1019,7 @@
 done
 
 
-text {* Permutations *}
+text \<open>Permutations\<close>
 
 lemma perm_map [intro]:
   assumes p: "a <~~> b"
@@ -1077,7 +1077,7 @@
     perm_setP[of _ _ "\<lambda>as. \<forall>a\<in>as. irreducible G a"]
 
 
-text {* Essentially equal factorizations *}
+text \<open>Essentially equal factorizations\<close>
 
 lemma (in monoid) essentially_equalI:
   assumes ex: "fs1 <~~> fs1'"  "fs1' [\<sim>] fs2"
@@ -1149,9 +1149,9 @@
 qed
 
 
-subsubsection {* Properties of lists of elements *}
-
-text {* Multiplication of factors in a list *}
+subsubsection \<open>Properties of lists of elements\<close>
+
+text \<open>Multiplication of factors in a list\<close>
 
 lemma (in monoid) multlist_closed [simp, intro]:
   assumes ascarr: "set fs \<subseteq> carrier G"
@@ -1224,7 +1224,7 @@
 done
 
 
-subsubsection {* Factorization in irreducible elements *}
+subsubsection \<open>Factorization in irreducible elements\<close>
 
 lemma wfactorsI:
   fixes G (structure)
@@ -1328,7 +1328,7 @@
 qed
 
 
-text {* Comparing wfactors *}
+text \<open>Comparing wfactors\<close>
 
 lemma (in comm_monoid_cancel) wfactors_listassoc_cong_l:
   assumes fact: "wfactors G fs a"
@@ -1389,7 +1389,7 @@
 qed
 
 
-subsubsection {* Essentially equal factorizations *}
+subsubsection \<open>Essentially equal factorizations\<close>
 
 lemma (in comm_monoid_cancel) unitfactor_ee:
   assumes uunit: "u \<in> Units G"
@@ -1719,7 +1719,7 @@
 qed
 
 
-subsubsection {* Factorial monoids and wfactors *}
+subsubsection \<open>Factorial monoids and wfactors\<close>
 
 lemma (in comm_monoid_cancel) factorial_monoidI:
   assumes wfactors_exists: 
@@ -1782,9 +1782,9 @@
 qed (blast intro: factors_wfactors wfactors_unique)
 
 
-subsection {* Factorizations as Multisets *}
-
-text {* Gives useful operations like intersection *}
+subsection \<open>Factorizations as Multisets\<close>
+
+text \<open>Gives useful operations like intersection\<close>
 
 (* FIXME: use class_of x instead of closure_of {x} *)
 
@@ -1795,7 +1795,7 @@
   "fmset G as = mset (map (\<lambda>a. assocs G a) as)"
 
 
-text {* Helper lemmas *}
+text \<open>Helper lemmas\<close>
 
 lemma (in monoid) assocs_repr_independence:
   assumes "y \<in> assocs G x"
@@ -1834,7 +1834,7 @@
     assocs_repr_independenceD[THEN assocs_assoc]
 
 
-subsubsection {* Comparing multisets *}
+subsubsection \<open>Comparing multisets\<close>
 
 lemma (in monoid) fmset_perm_cong:
   assumes prm: "as <~~> bs"
@@ -2022,7 +2022,7 @@
 by (fast intro: ee_fmset fmset_ee)
 
 
-subsubsection {* Interpreting multisets as factorizations *}
+subsubsection \<open>Interpreting multisets as factorizations\<close>
 
 lemma (in monoid) mset_fmsetEx:
   assumes elems: "\<And>X. X \<in> set_mset Cs \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"
@@ -2089,7 +2089,7 @@
 qed
 
 
-subsubsection {* Multiplication on multisets *}
+subsubsection \<open>Multiplication on multisets\<close>
 
 lemma (in factorial_monoid) mult_wfactors_fmset:
   assumes afs: "wfactors G as a" and bfs: "wfactors G bs b" and cfs: "wfactors G cs (a \<otimes> b)"
@@ -2131,7 +2131,7 @@
 qed
 
 
-subsubsection {* Divisibility on multisets *}
+subsubsection \<open>Divisibility on multisets\<close>
 
 lemma (in factorial_monoid) divides_fmsubset:
   assumes ab: "a divides b"
@@ -2215,7 +2215,7 @@
 by (blast intro: divides_fmsubset fmsubset_divides)
 
 
-text {* Proper factors on multisets *}
+text \<open>Proper factors on multisets\<close>
 
 lemma (in factorial_monoid) fmset_properfactor:
   assumes asubb: "fmset G as \<le># fmset G bs"
@@ -2250,7 +2250,7 @@
 apply (metis assms divides_fmsubset fmsubset_divides)
 done
 
-subsection {* Irreducible Elements are Prime *}
+subsection \<open>Irreducible Elements are Prime\<close>
 
 lemma (in factorial_monoid) irreducible_is_prime:
   assumes pirr: "irreducible G p"
@@ -2490,9 +2490,9 @@
 qed
 
 
-subsection {* Greatest Common Divisors and Lowest Common Multiples *}
-
-subsubsection {* Definitions *}
+subsection \<open>Greatest Common Divisors and Lowest Common Multiples\<close>
+
+subsubsection \<open>Definitions\<close>
 
 definition
   isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \<Rightarrow> bool"  ("(_ gcdof\<index> _ _)" [81,81,81] 80)
@@ -2529,7 +2529,7 @@
           "wf {(x, y). x \<in> carrier G \<and> y \<in> carrier G \<and> properfactor G x y}"
 
 
-subsubsection {* Connections to \texttt{Lattice.thy} *}
+subsubsection \<open>Connections to \texttt{Lattice.thy}\<close>
 
 lemma gcdof_greatestLower:
   fixes G (structure)
@@ -2571,7 +2571,7 @@
 by fast
 
 
-subsubsection {* Existence of gcd and lcm *}
+subsubsection \<open>Existence of gcd and lcm\<close>
 
 lemma (in factorial_monoid) gcdof_exists:
   assumes acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
@@ -2753,9 +2753,9 @@
 qed
 
 
-subsection {* Conditions for Factoriality *}
-
-subsubsection {* Gcd condition *}
+subsection \<open>Conditions for Factoriality\<close>
+
+subsubsection \<open>Gcd condition\<close>
 
 lemma (in gcd_condition_monoid) division_weak_lower_semilattice [simp]:
   shows "weak_lower_semilattice (division_rel G)"
@@ -3153,7 +3153,7 @@
   by (rule primeness_condition)
 
 
-subsubsection {* Divisor chain condition *}
+subsubsection \<open>Divisor chain condition\<close>
 
 lemma (in divisor_chain_condition_monoid) wfactors_exist:
   assumes acarr: "a \<in> carrier G"
@@ -3243,7 +3243,7 @@
 qed
 
 
-subsubsection {* Primeness condition *}
+subsubsection \<open>Primeness condition\<close>
 
 lemma (in comm_monoid_cancel) multlist_prime_pos:
   assumes carr: "a \<in> carrier G"  "set as \<subseteq> carrier G"
@@ -3481,9 +3481,9 @@
 done
 
 
-subsubsection {* Application to factorial monoids *}
-
-text {* Number of factors for wellfoundedness *}
+subsubsection \<open>Application to factorial monoids\<close>
+
+text \<open>Number of factors for wellfoundedness\<close>
 
 definition
   factorcount :: "_ \<Rightarrow> 'a \<Rightarrow> nat" where
@@ -3678,7 +3678,7 @@
 qed
 
 
-subsection {* Factoriality Theorems *}
+subsection \<open>Factoriality Theorems\<close>
 
 theorem factorial_condition_one: (* Jacobson theorem 2.21 *)
   shows "(divisor_chain_condition_monoid G \<and> primeness_condition_monoid G) = 
diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/Exponent.thy
--- a/src/HOL/Algebra/Exponent.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/Exponent.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -9,16 +9,16 @@
 imports Main "~~/src/HOL/Number_Theory/Primes"
 begin
 
-section {*Sylow's Theorem*}
+section \<open>Sylow's Theorem\<close>
 
-subsection {*The Combinatorial Argument Underlying the First Sylow Theorem*}
+subsection \<open>The Combinatorial Argument Underlying the First Sylow Theorem\<close>
 
 definition
   exponent :: "nat => nat => nat"
   where "exponent p s = (if prime p then (GREATEST r. p^r dvd s) else 0)"
 
 
-text{*Prime Theorems*}
+text\<open>Prime Theorems\<close>
 
 lemma prime_iff:
   "(prime p) = (Suc 0 < p & (\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))"
@@ -100,7 +100,7 @@
 done
 
 
-text{*Exponent Theorems*}
+text\<open>Exponent Theorems\<close>
 
 lemma exponent_ge [rule_format]:
   "[|p^k dvd n;  prime p;  0<n|] ==> k <= exponent p n"
@@ -182,7 +182,7 @@
 done
 
 
-text{*Main Combinatorial Argument*}
+text\<open>Main Combinatorial Argument\<close>
 
 lemma gcd_mult': fixes a::nat shows "gcd b (a * b) = b"
 by (simp add: mult.commute[of a b])
@@ -236,7 +236,7 @@
 apply (blast intro: exponent_equalityI p_fac_forw p_fac_backw)
 done
 
-text{*Suc rules that we have to delete from the simpset*}
+text\<open>Suc rules that we have to delete from the simpset\<close>
 lemmas bad_Sucs = binomial_Suc_Suc mult_Suc mult_Suc_right
 
 (*The bound K is needed; otherwise it's too weak to be used.*)
@@ -252,9 +252,9 @@
  prefer 2 apply (simp, clarify)
 apply (subgoal_tac "exponent p ((Suc (j+k) choose Suc k) * Suc k) =
                     exponent p (Suc k)")
- txt{*First, use the assumed equation.  We simplify the LHS to
+ txt\<open>First, use the assumed equation.  We simplify the LHS to
   @{term "exponent p (Suc (j + k) choose Suc k) + exponent p (Suc k)"}
-  the common terms cancel, proving the conclusion.*}
+  the common terms cancel, proving the conclusion.\<close>
  apply (simp del: bad_Sucs add: exponent_mult_add)
 apply (simp del: bad_Sucs add: mult_ac Suc_times_binomial exponent_mult_add)
 
@@ -297,14 +297,14 @@
  prefer 2 apply simp
 apply (subgoal_tac "0 < p^a * m & p^a <= p^a * m")
  prefer 2 apply (force simp add: prime_iff)
-txt{*A similar trick to the one used in @{text p_not_div_choose_lemma}:
+txt\<open>A similar trick to the one used in @{text p_not_div_choose_lemma}:
   insert an equation; use @{text exponent_mult_add} on the LHS; on the RHS,
   first
-  transform the binomial coefficient, then use @{text exponent_mult_add}.*}
+  transform the binomial coefficient, then use @{text exponent_mult_add}.\<close>
 apply (subgoal_tac "exponent p ((( (p^a) * m) choose p^a) * p^a) =
                     a + exponent p m")
  apply (simp add: exponent_mult_add)
-txt{*one subgoal left!*}
+txt\<open>one subgoal left!\<close>
 apply (auto simp: mult_ac)
 apply (subst times_binomial_minus1_eq, simp)
 apply (simp add: diff_le_mono exponent_mult_add)
diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -8,14 +8,14 @@
 imports Group
 begin
 
-subsection {* Product Operator for Commutative Monoids *}
+subsection \<open>Product Operator for Commutative Monoids\<close>
 
-subsubsection {* Inductive Definition of a Relation for Products over Sets *}
+subsubsection \<open>Inductive Definition of a Relation for Products over Sets\<close>
 
-text {* Instantiation of locale @{text LC} of theory @{text Finite_Set} is not
+text \<open>Instantiation of locale @{text LC} of theory @{text Finite_Set} is not
   possible, because here we have explicit typing rules like 
   @{text "x \<in> carrier G"}.  We introduce an explicit argument for the domain
-  @{text D}. *}
+  @{text D}.\<close>
 
 inductive_set
   foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set"
@@ -61,7 +61,7 @@
 qed
 
 
-text {* Left-Commutative Operations *}
+text \<open>Left-Commutative Operations\<close>
 
 locale LCD =
   fixes B :: "'b set"
@@ -111,7 +111,7 @@
   apply (erule foldSetD.cases)
    apply blast
   apply clarify
-  txt {* force simplification of @{text "card A < card (insert ...)"}. *}
+  txt \<open>force simplification of @{text "card A < card (insert ...)"}.\<close>
   apply (erule rev_mp)
   apply (simp add: less_Suc_eq_le)
   apply (rule impI)
@@ -119,7 +119,7 @@
    apply (subgoal_tac "Aa = Ab")
     prefer 2 apply (blast elim!: equalityE)
    apply blast
-  txt {* case @{prop "xa \<notin> xb"}. *}
+  txt \<open>case @{prop "xa \<notin> xb"}.\<close>
   apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb \<in> Aa & xa \<in> Ab")
    prefer 2 apply (blast elim!: equalityE)
   apply clarify
@@ -221,7 +221,7 @@
     ==> foldD D f e (A Un B) = foldD D f (foldD D f e B) A"
   by (simp add: foldD_nest_Un_Int)
 
--- {* Delete rules to do with @{text foldSetD} relation. *}
+-- \<open>Delete rules to do with @{text foldSetD} relation.\<close>
 
 declare foldSetD_imp_finite [simp del]
   empty_foldSetDE [rule del]
@@ -230,12 +230,12 @@
   foldSetD_closed [rule del]
 
 
-text {* Commutative Monoids *}
+text \<open>Commutative Monoids\<close>
 
-text {*
+text \<open>
   We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
   instead of @{text "'b => 'a => 'a"}.
-*}
+\<close>
 
 locale ACeD =
   fixes D :: "'a set"
@@ -263,7 +263,7 @@
 proof -
   assume "x \<in> D"
   then have "x \<cdot> e = x" by (rule ident)
-  with `x \<in> D` show ?thesis by (simp add: commute)
+  with \<open>x \<in> D\<close> show ?thesis by (simp add: commute)
 qed
 
 lemma (in ACeD) foldD_Un_Int:
@@ -285,7 +285,7 @@
     left_commute LCD.foldD_closed [OF LCD.intro [of D]])
 
 
-subsubsection {* Products over Finite Sets *}
+subsubsection \<open>Products over Finite Sets\<close>
 
 definition
   finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
@@ -299,7 +299,7 @@
       ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
 translations
   "\<Otimes>\<index>i\<in>A. b" \<rightleftharpoons> "CONST finprod \<struct>\<index> (%i. b) A"
-  -- {* Beware of argument permutation! *}
+  -- \<open>Beware of argument permutation!\<close>
 
 lemma (in comm_monoid) finprod_empty [simp]: 
   "finprod G f {} = \<one>"
@@ -367,7 +367,7 @@
   "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
      finprod G g (A Un B) \<otimes> finprod G g (A Int B) =
      finprod G g A \<otimes> finprod G g B"
--- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
+-- \<open>The reversed orientation looks more natural, but LOOPS as a simprule!\<close>
 proof (induct set: finite)
   case empty then show ?case by simp
 next
@@ -450,12 +450,12 @@
   (* This order of prems is slightly faster (3%) than the last two swapped. *)
   by (rule finprod_cong') (auto simp add: simp_implies_def)
 
-text {*Usually, if this rule causes a failed congruence proof error,
+text \<open>Usually, if this rule causes a failed congruence proof error,
   the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
   Adding @{thm [source] Pi_def} to the simpset is often useful.
   For this reason, @{thm [source] finprod_cong}
   is not added to the simpset by default.
-*}
+\<close>
 
 end
 
@@ -497,7 +497,7 @@
   case (infinite A)
   hence "\<not> finite (h ` A)"
     using finite_imageD by blast
-  with `\<not> finite A` show ?case by simp
+  with \<open>\<not> finite A\<close> show ?case by simp
 qed (auto simp add: Pi_def)
 
 lemma finprod_const:
diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/Group.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -8,13 +8,13 @@
 imports Lattice "~~/src/HOL/Library/FuncSet"
 begin
 
-section {* Monoids and Groups *}
+section \<open>Monoids and Groups\<close>
 
-subsection {* Definitions *}
+subsection \<open>Definitions\<close>
 
-text {*
+text \<open>
   Definitions follow @{cite "Jacobson:1985"}.
-*}
+\<close>
 
 record 'a monoid =  "'a partial_object" +
   mult    :: "['a, 'a] \<Rightarrow> 'a" (infixl "\<otimes>\<index>" 70)
@@ -26,7 +26,7 @@
 
 definition
   Units :: "_ => 'a set"
-  --{*The set of invertible elements*}
+  --\<open>The set of invertible elements\<close>
   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>)}"
 
 consts
@@ -187,7 +187,7 @@
   with G show ?thesis by (simp del: r_one add: m_assoc Units_closed)
 qed
 
-text {* Power *}
+text \<open>Power\<close>
 
 lemma (in monoid) nat_pow_closed [intro, simp]:
   "x \<in> carrier G ==> x (^) (n::nat) \<in> carrier G"
@@ -218,11 +218,11 @@
 (* Jacobson defines the order of a monoid here. *)
 
 
-subsection {* Groups *}
+subsection \<open>Groups\<close>
 
-text {*
+text \<open>
   A group is a monoid all of whose elements are invertible.
-*}
+\<close>
 
 locale group = monoid +
   assumes Units: "carrier G <= Units G"
@@ -321,7 +321,7 @@
   using Units_l_inv by simp
 
 
-subsection {* Cancellation Laws and Basic Properties *}
+subsection \<open>Cancellation Laws and Basic Properties\<close>
 
 lemma (in group) l_cancel [simp]:
   "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
@@ -397,7 +397,7 @@
   "\<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"
   by (metis inv_equality l_inv_ex l_one m_assoc r_inv)
 
-text {* Power *}
+text \<open>Power\<close>
 
 lemma (in group) int_pow_def2:
   "a (^) (z::int) = (if z < 0 then inv (a (^) (nat (-z))) else a (^) (nat z))"
@@ -435,7 +435,7 @@
 qed
 
  
-subsection {* Subgroups *}
+subsection \<open>Subgroups\<close>
 
 locale subgroup =
   fixes H and G (structure)
@@ -469,18 +469,18 @@
     done
 qed
 
-text {*
+text \<open>
   Since @{term H} is nonempty, it contains some element @{term x}.  Since
   it is closed under inverse, it contains @{text "inv x"}.  Since
   it is closed under product, it contains @{text "x \<otimes> inv x = \<one>"}.
-*}
+\<close>
 
 lemma (in group) one_in_subset:
   "[| 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 |]
    ==> \<one> \<in> H"
 by force
 
-text {* A characterization of subgroups: closed, non-empty subset. *}
+text \<open>A characterization of subgroups: closed, non-empty subset.\<close>
 
 lemma (in group) subgroupI:
   assumes subset: "H \<subseteq> carrier G" and non_empty: "H \<noteq> {}"
@@ -513,7 +513,7 @@
 *)
 
 
-subsection {* Direct Products *}
+subsection \<open>Direct Products\<close>
 
 definition
   DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid" (infixr "\<times>\<times>" 80) where
@@ -533,7 +533,7 @@
 qed
 
 
-text{*Does not use the previous result because it's easier just to use auto.*}
+text\<open>Does not use the previous result because it's easier just to use auto.\<close>
 lemma DirProd_group:
   assumes "group G" and "group H"
   shows "group (G \<times>\<times> H)"
@@ -571,7 +571,7 @@
 qed
 
 
-subsection {* Homomorphisms and Isomorphisms *}
+subsection \<open>Homomorphisms and Isomorphisms\<close>
 
 definition
   hom :: "_ => _ => ('a => 'b) set" where
@@ -611,8 +611,8 @@
 by (auto simp add: iso_def hom_def inj_on_def bij_betw_def)
 
 
-text{*Basis for homomorphism proofs: we assume two groups @{term G} and
-  @{term H}, with a homomorphism @{term h} between them*}
+text\<open>Basis for homomorphism proofs: we assume two groups @{term G} and
+  @{term H}, with a homomorphism @{term h} between them\<close>
 locale group_hom = G: group G + H: group H for G (structure) and H (structure) +
   fixes h
   assumes homh: "h \<in> hom G H"
@@ -665,13 +665,13 @@
   unfolding hom_def by (simp add: int_pow_mult)
 
 
-subsection {* Commutative Structures *}
+subsection \<open>Commutative Structures\<close>
 
-text {*
+text \<open>
   Naming convention: multiplicative structures that are commutative
   are called \emph{commutative}, additive structures are called
   \emph{Abelian}.
-*}
+\<close>
 
 locale comm_monoid = monoid +
   assumes m_comm: "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x \<otimes> y = y \<otimes> x"
@@ -753,9 +753,9 @@
   by (simp add: m_ac inv_mult_group)
 
 
-subsection {* The Lattice of Subgroups of a Group *}
+subsection \<open>The Lattice of Subgroups of a Group\<close>
 
-text_raw {* \label{sec:subgroup-lattice} *}
+text_raw \<open>\label{sec:subgroup-lattice}\<close>
 
 theorem (in group) subgroups_partial_order:
   "partial_order \<lparr>carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq>\<rparr>"
diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/Ideal.thy
--- a/src/HOL/Algebra/Ideal.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/Ideal.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -6,11 +6,11 @@
 imports Ring AbelCoset
 begin
 
-section {* Ideals *}
+section \<open>Ideals\<close>
 
-subsection {* Definitions *}
+subsection \<open>Definitions\<close>
 
-subsubsection {* General definition *}
+subsubsection \<open>General definition\<close>
 
 locale ideal = additive_subgroup I R + ring R for I and R (structure) +
   assumes I_l_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
@@ -44,12 +44,12 @@
 qed
 
 
-subsubsection (in ring) {* Ideals Generated by a Subset of @{term "carrier R"} *}
+subsubsection (in ring) \<open>Ideals Generated by a Subset of @{term "carrier R"}\<close>
 
 definition genideal :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set"  ("Idl\<index> _" [80] 79)
   where "genideal R S = Inter {I. ideal I R \<and> S \<subseteq> I}"
 
-subsubsection {* Principal Ideals *}
+subsubsection \<open>Principal Ideals\<close>
 
 locale principalideal = ideal +
   assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}"
@@ -70,7 +70,7 @@
 qed
 
 
-subsubsection {* Maximal Ideals *}
+subsubsection \<open>Maximal Ideals\<close>
 
 locale maximalideal = ideal +
   assumes I_notcarr: "carrier R \<noteq> I"
@@ -93,7 +93,7 @@
 qed
 
 
-subsubsection {* Prime Ideals *}
+subsubsection \<open>Prime Ideals\<close>
 
 locale primeideal = ideal + cring +
   assumes I_notcarr: "carrier R \<noteq> I"
@@ -140,7 +140,7 @@
 qed
 
 
-subsection {* Special Ideals *}
+subsection \<open>Special Ideals\<close>
 
 lemma (in ring) zeroideal: "ideal {\<zero>} R"
   apply (intro idealI subgroup.intro)
@@ -166,7 +166,7 @@
 qed
 
 
-subsection {* General Ideal Properies *}
+subsection \<open>General Ideal Properies\<close>
 
 lemma (in ideal) one_imp_carrier:
   assumes I_one_closed: "\<one> \<in> I"
@@ -187,10 +187,10 @@
   using iI by (rule a_Hcarr)
 
 
-subsection {* Intersection of Ideals *}
+subsection \<open>Intersection of Ideals\<close>
 
-text {* \paragraph{Intersection of two ideals} The intersection of any
-  two ideals is again an ideal in @{term R} *}
+text \<open>\paragraph{Intersection of two ideals} The intersection of any
+  two ideals is again an ideal in @{term R}\<close>
 lemma (in ring) i_intersect:
   assumes "ideal I R"
   assumes "ideal J R"
@@ -212,8 +212,8 @@
     done
 qed
 
-text {* The intersection of any Number of Ideals is again
-        an Ideal in @{term R} *}
+text \<open>The intersection of any Number of Ideals is again
+        an Ideal in @{term R}\<close>
 lemma (in ring) i_Intersect:
   assumes Sideals: "\<And>I. I \<in> S \<Longrightarrow> ideal I R"
     and notempty: "S \<noteq> {}"
@@ -291,7 +291,7 @@
 qed
 
 
-subsection {* Addition of Ideals *}
+subsection \<open>Addition of Ideals\<close>
 
 lemma (in ring) add_ideals:
   assumes idealI: "ideal I R"
@@ -335,9 +335,9 @@
 qed
 
 
-subsection (in ring) {* Ideals generated by a subset of @{term "carrier R"} *}
+subsection (in ring) \<open>Ideals generated by a subset of @{term "carrier R"}\<close>
 
-text {* @{term genideal} generates an ideal *}
+text \<open>@{term genideal} generates an ideal\<close>
 lemma (in ring) genideal_ideal:
   assumes Scarr: "S \<subseteq> carrier R"
   shows "ideal (Idl S) R"
@@ -360,14 +360,14 @@
   then show "i \<in> Idl {i}" by fast
 qed
 
-text {* @{term genideal} generates the minimal ideal *}
+text \<open>@{term genideal} generates the minimal ideal\<close>
 lemma (in ring) genideal_minimal:
   assumes a: "ideal I R"
     and b: "S \<subseteq> I"
   shows "Idl S \<subseteq> I"
   unfolding genideal_def by rule (elim InterD, simp add: a b)
 
-text {* Generated ideals and subsets *}
+text \<open>Generated ideals and subsets\<close>
 lemma (in ring) Idl_subset_ideal:
   assumes Iideal: "ideal I R"
     and Hcarr: "H \<subseteq> carrier R"
@@ -425,12 +425,12 @@
 qed
 
 
-text {* Generation of Principal Ideals in Commutative Rings *}
+text \<open>Generation of Principal Ideals in Commutative Rings\<close>
 
 definition cgenideal :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set"  ("PIdl\<index> _" [80] 79)
   where "cgenideal R a = {x \<otimes>\<^bsub>R\<^esub> a | x. x \<in> carrier R}"
 
-text {* genhideal (?) really generates an ideal *}
+text \<open>genhideal (?) really generates an ideal\<close>
 lemma (in cring) cgenideal_ideal:
   assumes acarr: "a \<in> carrier R"
   shows "ideal (PIdl a) R"
@@ -499,7 +499,7 @@
     by fast
 qed
 
-text {* @{const "cgenideal"} is minimal *}
+text \<open>@{const "cgenideal"} is minimal\<close>
 
 lemma (in ring) cgenideal_minimal:
   assumes "ideal J R"
@@ -544,7 +544,7 @@
 qed
 
 
-subsection {* Union of Ideals *}
+subsection \<open>Union of Ideals\<close>
 
 lemma (in ring) union_genideal:
   assumes idealI: "ideal I R"
@@ -589,16 +589,16 @@
 qed
 
 
-subsection {* Properties of Principal Ideals *}
+subsection \<open>Properties of Principal Ideals\<close>
 
-text {* @{text "\<zero>"} generates the zero ideal *}
+text \<open>@{text "\<zero>"} generates the zero ideal\<close>
 lemma (in ring) zero_genideal: "Idl {\<zero>} = {\<zero>}"
   apply rule
   apply (simp add: genideal_minimal zeroideal)
   apply (fast intro!: genideal_self)
   done
 
-text {* @{text "\<one>"} generates the unit ideal *}
+text \<open>@{text "\<one>"} generates the unit ideal\<close>
 lemma (in ring) one_genideal: "Idl {\<one>} = carrier R"
 proof -
   have "\<one> \<in> Idl {\<one>}"
@@ -608,14 +608,14 @@
 qed
 
 
-text {* The zero ideal is a principal ideal *}
+text \<open>The zero ideal is a principal ideal\<close>
 corollary (in ring) zeropideal: "principalideal {\<zero>} R"
   apply (rule principalidealI)
    apply (rule zeroideal)
   apply (blast intro!: zero_genideal[symmetric])
   done
 
-text {* The unit ideal is a principal ideal *}
+text \<open>The unit ideal is a principal ideal\<close>
 corollary (in ring) onepideal: "principalideal (carrier R) R"
   apply (rule principalidealI)
    apply (rule oneideal)
@@ -623,7 +623,7 @@
   done
 
 
-text {* Every principal ideal is a right coset of the carrier *}
+text \<open>Every principal ideal is a right coset of the carrier\<close>
 lemma (in principalideal) rcos_generate:
   assumes "cring R"
   shows "\<exists>x\<in>I. I = carrier R #> x"
@@ -650,7 +650,7 @@
 qed
 
 
-subsection {* Prime Ideals *}
+subsection \<open>Prime Ideals\<close>
 
 lemma (in ideal) primeidealCD:
   assumes "cring R"
@@ -683,7 +683,7 @@
   then show thesis using primeidealCD [OF R.is_cring notprime] by blast
 qed
 
-text {* If @{text "{\<zero>}"} is a prime ideal of a commutative ring, the ring is a domain *}
+text \<open>If @{text "{\<zero>}"} is a prime ideal of a commutative ring, the ring is a domain\<close>
 lemma (in cring) zeroprimeideal_domainI:
   assumes pi: "primeideal {\<zero>} R"
   shows "domain R"
@@ -713,7 +713,7 @@
   done
 
 
-subsection {* Maximal Ideals *}
+subsection \<open>Maximal Ideals\<close>
 
 lemma (in ideal) helper_I_closed:
   assumes carr: "a \<in> carrier R" "x \<in> carrier R" "y \<in> carrier R"
@@ -767,7 +767,7 @@
   qed
 qed
 
-text {* In a cring every maximal ideal is prime *}
+text \<open>In a cring every maximal ideal is prime\<close>
 lemma (in cring) maximalideal_is_prime:
   assumes "maximalideal I R"
   shows "primeideal I R"
@@ -825,7 +825,7 @@
 qed
 
 
-subsection {* Derived Theorems *}
+subsection \<open>Derived Theorems\<close>
 
 --"A non-zero cring that has only the two trivial ideals is a field"
 lemma (in cring) trivialideals_fieldI:
@@ -927,7 +927,7 @@
   by (fast intro!: trivialideals_fieldI[OF carrnzero] field.all_ideals)
 
 
-text {* Like zeroprimeideal for domains *}
+text \<open>Like zeroprimeideal for domains\<close>
 lemma (in field) zeromaximalideal: "maximalideal {\<zero>} R"
   apply (rule maximalidealI)
     apply (rule zeroideal)
diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/IntRing.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -7,9 +7,9 @@
 imports QuotRing Lattice Int "~~/src/HOL/Number_Theory/Primes"
 begin
 
-section {* The Ring of Integers *}
+section \<open>The Ring of Integers\<close>
 
-subsection {* Some properties of @{typ int} *}
+subsection \<open>Some properties of @{typ int}\<close>
 
 lemma dvds_eq_abseq:
   fixes k :: int
@@ -20,7 +20,7 @@
 done
 
 
-subsection {* @{text "\<Z>"}: The Set of Integers as Algebraic Structure *}
+subsection \<open>@{text "\<Z>"}: The Set of Integers as Algebraic Structure\<close>
 
 abbreviation int_ring :: "int ring" ("\<Z>")
   where "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
@@ -47,11 +47,11 @@
 *)
 
 
-subsection {* Interpretations *}
+subsection \<open>Interpretations\<close>
 
-text {* Since definitions of derived operations are global, their
+text \<open>Since definitions of derived operations are global, their
   interpretation needs to be done as early as possible --- that is,
-  with as few assumptions as possible. *}
+  with as few assumptions as possible.\<close>
 
 interpretation int: monoid \<Z>
   where "carrier \<Z> = UNIV"
@@ -159,8 +159,8 @@
 qed (simp add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq int_a_inv_eq int_a_minus_eq)+
 
 
-text {* Removal of occurrences of @{term UNIV} in interpretation result
-  --- experimental. *}
+text \<open>Removal of occurrences of @{term UNIV} in interpretation result
+  --- experimental.\<close>
 
 lemma UNIV:
   "x \<in> UNIV \<longleftrightarrow> True"
@@ -218,7 +218,7 @@
   by standard clarsimp
 
 
-subsection {* Generated Ideals of @{text "\<Z>"} *}
+subsection \<open>Generated Ideals of @{text "\<Z>"}\<close>
 
 lemma int_Idl: "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}"
   apply (subst int.cgenideal_eq_genideal[symmetric]) apply simp
@@ -255,7 +255,7 @@
 qed
 
 
-subsection {* Ideals and Divisibility *}
+subsection \<open>Ideals and Divisibility\<close>
 
 lemma int_Idl_subset_ideal: "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})"
   by (rule int.Idl_subset_ideal') simp_all
@@ -287,7 +287,7 @@
   done
 
 
-subsection {* Ideals and the Modulus *}
+subsection \<open>Ideals and the Modulus\<close>
 
 definition ZMod :: "int \<Rightarrow> int \<Rightarrow> int set"
   where "ZMod k r = (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
@@ -370,7 +370,7 @@
   done
 
 
-subsection {* Factorization *}
+subsection \<open>Factorization\<close>
 
 definition ZFact :: "int \<Rightarrow> int set ring"
   where "ZFact k = \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/Lattice.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -9,9 +9,9 @@
 imports Congruence
 begin
 
-section {* Orders and Lattices *}
+section \<open>Orders and Lattices\<close>
 
-subsection {* Partial Orders *}
+subsection \<open>Partial Orders\<close>
 
 record 'a gorder = "'a eq_object" +
   le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
@@ -32,7 +32,7 @@
   where "x \<sqsubset>\<^bsub>L\<^esub> y \<longleftrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> y & x .\<noteq>\<^bsub>L\<^esub> y"
 
 
-subsubsection {* The order relation *}
+subsubsection \<open>The order relation\<close>
 
 context weak_partial_order
 begin
@@ -103,7 +103,7 @@
   using assms unfolding lless_def by (blast dest: le_trans intro: sym)
 
 
-subsubsection {* Upper and lower bounds of a set *}
+subsubsection \<open>Upper and lower bounds of a set\<close>
 
 definition
   Upper :: "[_, 'a set] => 'a set"
@@ -276,7 +276,7 @@
 qed
 
 
-subsubsection {* Least and greatest, as predicate *}
+subsubsection \<open>Least and greatest, as predicate\<close>
 
 definition
   least :: "[_, 'a, 'a set] => bool"
@@ -286,8 +286,8 @@
   greatest :: "[_, 'a, 'a set] => bool"
   where "greatest L g A \<longleftrightarrow> A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq>\<^bsub>L\<^esub> g)"
 
-text (in weak_partial_order) {* Could weaken these to @{term "l \<in> carrier L \<and> l
-  .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}. *}
+text (in weak_partial_order) \<open>Could weaken these to @{term "l \<in> carrier L \<and> l
+  .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}.\<close>
 
 lemma least_closed [intro, simp]:
   "least L l A ==> l \<in> carrier L"
@@ -310,8 +310,8 @@
   "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> least L x A = least L x' A"
   by (unfold least_def) (auto dest: sym)
 
-text (in weak_partial_order) {* @{const least} is not congruent in the second parameter for 
-  @{term "A {.=} A'"} *}
+text (in weak_partial_order) \<open>@{const least} is not congruent in the second parameter for 
+  @{term "A {.=} A'"}\<close>
 
 lemma (in weak_partial_order) least_Upper_cong_l:
   assumes "x .= x'"
@@ -367,8 +367,8 @@
   greatest L x A = greatest L x' A"
   by (unfold greatest_def) (auto dest: sym)
 
-text (in weak_partial_order) {* @{const greatest} is not congruent in the second parameter for 
-  @{term "A {.=} A'"} *}
+text (in weak_partial_order) \<open>@{const greatest} is not congruent in the second parameter for 
+  @{term "A {.=} A'"}\<close>
 
 lemma (in weak_partial_order) greatest_Lower_cong_l:
   assumes "x .= x'"
@@ -402,7 +402,7 @@
   shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
   by (unfold greatest_def) blast
 
-text {* Supremum and infimum *}
+text \<open>Supremum and infimum\<close>
 
 definition
   sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
@@ -421,7 +421,7 @@
   where "x \<sqinter>\<^bsub>L\<^esub> y = \<Sqinter>\<^bsub>L\<^esub>{x, y}"
 
 
-subsection {* Lattices *}
+subsection \<open>Lattices\<close>
 
 locale weak_upper_semilattice = weak_partial_order +
   assumes sup_of_two_exists:
@@ -434,7 +434,7 @@
 locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice
 
 
-subsubsection {* Supremum *}
+subsubsection \<open>Supremum\<close>
 
 lemma (in weak_upper_semilattice) joinI:
   "[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |]
@@ -507,7 +507,7 @@
   unfolding sup_def
   by (rule someI2) (auto intro: sup_of_singletonI)
 
-text {* Condition on @{text A}: supremum exists. *}
+text \<open>Condition on @{text A}: supremum exists.\<close>
 
 lemma (in weak_upper_semilattice) sup_insertI:
   "[| !!s. least L s (Upper L (insert x A)) ==> P s;
@@ -638,7 +638,7 @@
   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   shows "x \<squnion> (y \<squnion> z) .= \<Squnion>{x, y, z}"
 proof (rule finite_sup_insertI)
-  -- {* The textbook argument in Jacobson I, p 457 *}
+  -- \<open>The textbook argument in Jacobson I, p 457\<close>
   fix s
   assume sup: "least L s (Upper L {x, y, z})"
   show "x \<squnion> (y \<squnion> z) .= s"
@@ -652,7 +652,7 @@
   qed (simp_all add: L least_closed [OF sup])
 qed (simp_all add: L)
 
-text {* Commutativity holds for @{text "="}. *}
+text \<open>Commutativity holds for @{text "="}.\<close>
 
 lemma join_comm:
   fixes L (structure)
@@ -673,7 +673,7 @@
 qed
 
 
-subsubsection {* Infimum *}
+subsubsection \<open>Infimum\<close>
 
 lemma (in weak_lower_semilattice) meetI:
   "[| !!i. greatest L i (Lower L {x, y}) ==> P i;
@@ -747,7 +747,7 @@
   unfolding inf_def
   by (rule someI2) (auto intro: inf_of_singletonI)
 
-text {* Condition on @{text A}: infimum exists. *}
+text \<open>Condition on @{text A}: infimum exists.\<close>
 
 lemma (in weak_lower_semilattice) inf_insertI:
   "[| !!i. greatest L i (Lower L (insert x A)) ==> P i;
@@ -879,7 +879,7 @@
   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   shows "x \<sqinter> (y \<sqinter> z) .= \<Sqinter>{x, y, z}"
 proof (rule finite_inf_insertI)
-  txt {* The textbook argument in Jacobson I, p 457 *}
+  txt \<open>The textbook argument in Jacobson I, p 457\<close>
   fix i
   assume inf: "greatest L i (Lower L {x, y, z})"
   show "x \<sqinter> (y \<sqinter> z) .= i"
@@ -911,19 +911,19 @@
 qed
 
 
-subsection {* Total Orders *}
+subsection \<open>Total Orders\<close>
 
 locale weak_total_order = weak_partial_order +
   assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
 
-text {* Introduction rule: the usual definition of total order *}
+text \<open>Introduction rule: the usual definition of total order\<close>
 
 lemma (in weak_partial_order) weak_total_orderI:
   assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   shows "weak_total_order L"
   by standard (rule total)
 
-text {* Total orders are lattices. *}
+text \<open>Total orders are lattices.\<close>
 
 sublocale weak_total_order < weak: weak_lattice
 proof
@@ -969,7 +969,7 @@
 qed
 
 
-subsection {* Complete Lattices *}
+subsection \<open>Complete Lattices\<close>
 
 locale weak_complete_lattice = weak_lattice +
   assumes sup_exists:
@@ -977,7 +977,7 @@
     and inf_exists:
     "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
 
-text {* Introduction rule: the usual definition of complete lattice *}
+text \<open>Introduction rule: the usual definition of complete lattice\<close>
 
 lemma (in weak_partial_order) weak_complete_latticeI:
   assumes sup_exists:
@@ -1034,7 +1034,7 @@
   "\<bottom> \<in> carrier L"
   by (unfold bottom_def) simp
 
-text {* Jacobson: Theorem 8.1 *}
+text \<open>Jacobson: Theorem 8.1\<close>
 
 lemma Lower_empty [simp]:
   "Lower L {} = carrier L"
@@ -1090,7 +1090,7 @@
 (* TODO: prove dual version *)
 
 
-subsection {* Orders and Lattices where @{text eq} is the Equality *}
+subsection \<open>Orders and Lattices where @{text eq} is the Equality\<close>
 
 locale partial_order = weak_partial_order +
   assumes eq_is_equal: "op .= = op ="
@@ -1115,7 +1115,7 @@
 end
 
 
-text {* Least and greatest, as predicate *}
+text \<open>Least and greatest, as predicate\<close>
 
 lemma (in partial_order) least_unique:
   "[| least L x A; least L y A |] ==> x = y"
@@ -1126,7 +1126,7 @@
   using weak_greatest_unique unfolding eq_is_equal .
 
 
-text {* Lattices *}
+text \<open>Lattices\<close>
 
 locale upper_semilattice = partial_order +
   assumes sup_of_two_exists:
@@ -1145,7 +1145,7 @@
 locale lattice = upper_semilattice + lower_semilattice
 
 
-text {* Supremum *}
+text \<open>Supremum\<close>
 
 declare (in partial_order) weak_sup_of_singleton [simp del]
 
@@ -1164,7 +1164,7 @@
   using weak_join_assoc L unfolding eq_is_equal .
 
 
-text {* Infimum *}
+text \<open>Infimum\<close>
 
 declare (in partial_order) weak_inf_of_singleton [simp del]
 
@@ -1172,7 +1172,7 @@
   "x \<in> carrier L ==> \<Sqinter>{x} = x"
   using weak_inf_of_singleton unfolding eq_is_equal .
 
-text {* Condition on @{text A}: infimum exists. *}
+text \<open>Condition on @{text A}: infimum exists.\<close>
 
 lemma (in lower_semilattice) meet_assoc_lemma:
   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
@@ -1185,7 +1185,7 @@
   using weak_meet_assoc L unfolding eq_is_equal .
 
 
-text {* Total Orders *}
+text \<open>Total Orders\<close>
 
 locale total_order = partial_order +
   assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
@@ -1193,20 +1193,20 @@
 sublocale total_order < weak: weak_total_order
   by standard (rule total_order_total)
 
-text {* Introduction rule: the usual definition of total order *}
+text \<open>Introduction rule: the usual definition of total order\<close>
 
 lemma (in partial_order) total_orderI:
   assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   shows "total_order L"
   by standard (rule total)
 
-text {* Total orders are lattices. *}
+text \<open>Total orders are lattices.\<close>
 
 sublocale total_order < weak: lattice
   by standard (auto intro: sup_of_two_exists inf_of_two_exists)
 
 
-text {* Complete lattices *}
+text \<open>Complete lattices\<close>
 
 locale complete_lattice = lattice +
   assumes sup_exists:
@@ -1217,7 +1217,7 @@
 sublocale complete_lattice < weak: weak_complete_lattice
   by standard (auto intro: sup_exists inf_exists)
 
-text {* Introduction rule: the usual definition of complete lattice *}
+text \<open>Introduction rule: the usual definition of complete lattice\<close>
 
 lemma (in partial_order) complete_latticeI:
   assumes sup_exists:
@@ -1273,9 +1273,9 @@
 (* TODO: prove dual version *)
 
 
-subsection {* Examples *}
+subsection \<open>Examples\<close>
 
-subsubsection {* The Powerset of a Set is a Complete Lattice *}
+subsubsection \<open>The Powerset of a Set is a Complete Lattice\<close>
 
 theorem powerset_is_complete_lattice:
   "complete_lattice \<lparr>carrier = Pow A, eq = op =, le = op \<subseteq>\<rparr>"
@@ -1293,13 +1293,13 @@
   fix B
   assume "B \<subseteq> carrier ?L"
   then have "greatest ?L (\<Inter>B \<inter> A) (Lower ?L B)"
-    txt {* @{term "\<Inter>B"} is not the infimum of @{term B}:
-      @{term "\<Inter>{} = UNIV"} which is in general bigger than @{term "A"}! *}
+    txt \<open>@{term "\<Inter>B"} is not the infimum of @{term B}:
+      @{term "\<Inter>{} = UNIV"} which is in general bigger than @{term "A"}!\<close>
     by (fastforce intro!: greatest_LowerI simp: Lower_def)
   then show "EX i. greatest ?L i (Lower ?L B)" ..
 qed
 
-text {* An other example, that of the lattice of subgroups of a group,
-  can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *}
+text \<open>An other example, that of the lattice of subgroups of a group,
+  can be found in Group theory (Section~\ref{sec:subgroup-lattice}).\<close>
 
 end
diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/Module.thy
--- a/src/HOL/Algebra/Module.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/Module.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -7,9 +7,9 @@
 imports Ring
 begin
 
-section {* Modules over an Abelian Group *}
+section \<open>Modules over an Abelian Group\<close>
 
-subsection {* Definitions *}
+subsection \<open>Definitions\<close>
 
 record ('a, 'b) module = "'b ring" +
   smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)
@@ -103,7 +103,7 @@
     smult_l_distr smult_r_distr smult_assoc1)
 
 
-subsection {* Basic Properties of Algebras *}
+subsection \<open>Basic Properties of Algebras\<close>
 
 lemma (in algebra) smult_l_null [simp]:
   "x \<in> carrier M ==> \<zero> \<odot>\<^bsub>M\<^esub> x = \<zero>\<^bsub>M\<^esub>"
diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/QuotRing.thy
--- a/src/HOL/Algebra/QuotRing.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/QuotRing.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -6,17 +6,17 @@
 imports RingHom
 begin
 
-section {* Quotient Rings *}
+section \<open>Quotient Rings\<close>
 
-subsection {* Multiplication on Cosets *}
+subsection \<open>Multiplication on Cosets\<close>
 
 definition rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set"
     ("[mod _:] _ \<Otimes>\<index> _" [81,81,81] 80)
   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))"
 
 
-text {* @{const "rcoset_mult"} fulfils the properties required by
-  congruences *}
+text \<open>@{const "rcoset_mult"} fulfils the properties required by
+  congruences\<close>
 lemma (in ideal) rcoset_mult_add:
     "x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> [mod I:] (I +> x) \<Otimes> (I +> y) = I +> (x \<otimes> y)"
   apply rule
@@ -70,7 +70,7 @@
 qed
 
 
-subsection {* Quotient Ring Definition *}
+subsection \<open>Quotient Ring Definition\<close>
 
 definition FactRing :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) ring"
     (infixl "Quot" 65)
@@ -79,33 +79,33 @@
       one = (I +>\<^bsub>R\<^esub> \<one>\<^bsub>R\<^esub>), zero = I, add = set_add R\<rparr>"
 
 
-subsection {* Factorization over General Ideals *}
+subsection \<open>Factorization over General Ideals\<close>
 
-text {* The quotient is a ring *}
+text \<open>The quotient is a ring\<close>
 lemma (in ideal) quotient_is_ring: "ring (R Quot I)"
 apply (rule ringI)
-   --{* abelian group *}
+   --\<open>abelian group\<close>
    apply (rule comm_group_abelian_groupI)
    apply (simp add: FactRing_def)
    apply (rule a_factorgroup_is_comm_group[unfolded A_FactGroup_def'])
-  --{* mult monoid *}
+  --\<open>mult monoid\<close>
   apply (rule monoidI)
       apply (simp_all add: FactRing_def A_RCOSETS_def RCOSETS_def
              a_r_coset_def[symmetric])
-      --{* mult closed *}
+      --\<open>mult closed\<close>
       apply (clarify)
       apply (simp add: rcoset_mult_add, fast)
-     --{* mult @{text one_closed} *}
+     --\<open>mult @{text one_closed}\<close>
      apply force
-    --{* mult assoc *}
+    --\<open>mult assoc\<close>
     apply clarify
     apply (simp add: rcoset_mult_add m_assoc)
-   --{* mult one *}
+   --\<open>mult one\<close>
    apply clarify
    apply (simp add: rcoset_mult_add)
   apply clarify
   apply (simp add: rcoset_mult_add)
- --{* distr *}
+ --\<open>distr\<close>
  apply clarify
  apply (simp add: rcoset_mult_add a_rcos_sum l_distr)
 apply clarify
@@ -113,7 +113,7 @@
 done
 
 
-text {* This is a ring homomorphism *}
+text \<open>This is a ring homomorphism\<close>
 
 lemma (in ideal) rcos_ring_hom: "(op +> I) \<in> ring_hom R (R Quot I)"
 apply (rule ring_hom_memI)
@@ -132,7 +132,7 @@
 apply (simp add: FactRing_def)
 done
 
-text {* The quotient of a cring is also commutative *}
+text \<open>The quotient of a cring is also commutative\<close>
 lemma (in ideal) quotient_is_cring:
   assumes "cring R"
   shows "cring (R Quot I)"
@@ -148,7 +148,7 @@
     done
 qed
 
-text {* Cosets as a ring homomorphism on crings *}
+text \<open>Cosets as a ring homomorphism on crings\<close>
 lemma (in ideal) rcos_ring_hom_cring:
   assumes "cring R"
   shows "ring_hom_cring R (R Quot I) (op +> I)"
@@ -164,9 +164,9 @@
 qed
 
 
-subsection {* Factorization over Prime Ideals *}
+subsection \<open>Factorization over Prime Ideals\<close>
 
-text {* The quotient ring generated by a prime ideal is a domain *}
+text \<open>The quotient ring generated by a prime ideal is a domain\<close>
 lemma (in primeideal) quotient_is_domain: "domain (R Quot I)"
   apply (rule domain.intro)
    apply (rule quotient_is_cring, rule is_cring)
@@ -201,18 +201,18 @@
   then show "I +> x = I" by (rule a_rcos_const)
 qed
 
-text {* Generating right cosets of a prime ideal is a homomorphism
-        on commutative rings *}
+text \<open>Generating right cosets of a prime ideal is a homomorphism
+        on commutative rings\<close>
 lemma (in primeideal) rcos_ring_hom_cring: "ring_hom_cring R (R Quot I) (op +> I)"
   by (rule rcos_ring_hom_cring) (rule is_cring)
 
 
-subsection {* Factorization over Maximal Ideals *}
+subsection \<open>Factorization over Maximal Ideals\<close>
 
-text {* In a commutative ring, the quotient ring over a maximal ideal
+text \<open>In a commutative ring, the quotient ring over a maximal ideal
         is a field.
         The proof follows ``W. Adkins, S. Weintraub: Algebra --
-        An Approach via Module Theory'' *}
+        An Approach via Module Theory''\<close>
 lemma (in maximalideal) quotient_is_field:
   assumes "cring R"
   shows "field (R Quot I)"
@@ -225,7 +225,7 @@
      apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarsimp)
      apply (simp add: rcoset_mult_add) defer 1
   proof (rule ccontr, simp)
-    --{* Quotient is not empty *}
+    --\<open>Quotient is not empty\<close>
     assume "\<zero>\<^bsub>R Quot I\<^esub> = \<one>\<^bsub>R Quot I\<^esub>"
     then have II1: "I = I +> \<one>" by (simp add: FactRing_def)
     from a_rcos_self[OF one_closed] have "\<one> \<in> I"
@@ -233,11 +233,11 @@
     then have "I = carrier R" by (rule one_imp_carrier)
     with I_notcarr show False by simp
   next
-    --{* Existence of Inverse *}
+    --\<open>Existence of Inverse\<close>
     fix a
     assume IanI: "I +> a \<noteq> I" and acarr: "a \<in> carrier R"
 
-    --{* Helper ideal @{text "J"} *}
+    --\<open>Helper ideal @{text "J"}\<close>
     def J \<equiv> "(carrier R #> a) <+> I :: 'a set"
     have idealJ: "ideal J R"
       apply (unfold J_def, rule add_ideals)
@@ -245,7 +245,7 @@
       apply (rule is_ideal)
       done
 
-    --{* Showing @{term "J"} not smaller than @{term "I"} *}
+    --\<open>Showing @{term "J"} not smaller than @{term "I"}\<close>
     have IinJ: "I \<subseteq> J"
     proof (rule, simp add: J_def r_coset_def set_add_defs)
       fix x
@@ -256,7 +256,7 @@
       with Zcarr and xI show "\<exists>xa\<in>carrier R. \<exists>k\<in>I. x = xa \<otimes> a \<oplus> k" by fast
     qed
 
-    --{* Showing @{term "J \<noteq> I"} *}
+    --\<open>Showing @{term "J \<noteq> I"}\<close>
     have anI: "a \<notin> I"
     proof (rule ccontr, simp)
       assume "a \<in> I"
@@ -274,7 +274,7 @@
 
     from aJ and anI have JnI: "J \<noteq> I" by fast
 
-    --{* Deducing @{term "J = carrier R"} because @{term "I"} is maximal *}
+    --\<open>Deducing @{term "J = carrier R"} because @{term "I"} is maximal\<close>
     from idealJ and IinJ have "J = I \<or> J = carrier R"
     proof (rule I_maximal, unfold J_def)
       have "carrier R #> a \<subseteq> carrier R"
@@ -285,7 +285,7 @@
 
     with JnI have Jcarr: "J = carrier R" by simp
 
-    --{* Calculating an inverse for @{term "a"} *}
+    --\<open>Calculating an inverse for @{term "a"}\<close>
     from one_closed[folded Jcarr]
     have "\<exists>r\<in>carrier R. \<exists>i\<in>I. \<one> = r \<otimes> a \<oplus> i"
       by (simp add: J_def r_coset_def set_add_defs)
@@ -294,7 +294,7 @@
     from one and rcarr and acarr and iI[THEN a_Hcarr]
     have rai1: "a \<otimes> r = \<ominus>i \<oplus> \<one>" by algebra
 
-    --{* Lifting to cosets *}
+    --\<open>Lifting to cosets\<close>
     from iI have "\<ominus>i \<oplus> \<one> \<in> I +> \<one>"
       by (intro a_rcosI, simp, intro a_subset, simp)
     with rai1 have "a \<otimes> r \<in> I +> \<one>" by simp
diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/Ring.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -7,15 +7,15 @@
 imports FiniteProduct
 begin
 
-section {* The Algebraic Hierarchy of Rings *}
+section \<open>The Algebraic Hierarchy of Rings\<close>
 
-subsection {* Abelian Groups *}
+subsection \<open>Abelian Groups\<close>
 
 record 'a ring = "'a monoid" +
   zero :: 'a ("\<zero>\<index>")
   add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65)
 
-text {* Derived operations. *}
+text \<open>Derived operations.\<close>
 
 definition
   a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
@@ -39,7 +39,7 @@
       ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
 translations
   "\<Oplus>\<index>i\<in>A. b" \<rightleftharpoons> "CONST finsum \<struct>\<index> (%i. b) A"
-  -- {* Beware of argument permutation! *}
+  -- \<open>Beware of argument permutation!\<close>
 
 
 locale abelian_group = abelian_monoid +
@@ -47,7 +47,7 @@
      "comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
 
 
-subsection {* Basic Properties *}
+subsection \<open>Basic Properties\<close>
 
 lemma abelian_monoidI:
   fixes R (structure)
@@ -91,7 +91,7 @@
 
 lemmas monoid_record_simps = partial_object.simps monoid.simps
 
-text {* Transfer facts from multiplicative structures via interpretation. *}
+text \<open>Transfer facts from multiplicative structures via interpretation.\<close>
 
 sublocale abelian_monoid <
   add!: monoid "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
@@ -140,9 +140,9 @@
 lemmas finsum_infinite = add.finprod_infinite
 
 lemmas finsum_cong = add.finprod_cong
-text {*Usually, if this rule causes a failed congruence proof error,
+text \<open>Usually, if this rule causes a failed congruence proof error,
    the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
-   Adding @{thm [source] Pi_def} to the simpset is often useful. *}
+   Adding @{thm [source] Pi_def} to the simpset is often useful.\<close>
 
 lemmas finsum_reindex = add.finprod_reindex
 
@@ -206,7 +206,7 @@
 
 lemmas (in abelian_group) minus_add = add.inv_mult
  
-text {* Derive an @{text "abelian_group"} from a @{text "comm_group"} *}
+text \<open>Derive an @{text "abelian_group"} from a @{text "comm_group"}\<close>
 
 lemma comm_group_abelian_groupI:
   fixes G (structure)
@@ -219,7 +219,7 @@
 qed
 
 
-subsection {* Rings: Basic Definitions *}
+subsection \<open>Rings: Basic Definitions\<close>
 
 locale semiring = abelian_monoid R + monoid R for R (structure) +
   assumes l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
@@ -246,7 +246,7 @@
   assumes field_Units: "Units R = carrier R - {\<zero>}"
 
 
-subsection {* Rings *}
+subsection \<open>Rings\<close>
 
 lemma ringI:
   fixes R (structure)
@@ -283,8 +283,8 @@
   shows "cring R"
 proof (intro cring.intro ring.intro)
   show "ring_axioms R"
-    -- {* Right-distributivity follows from left-distributivity and
-          commutativity. *}
+    -- \<open>Right-distributivity follows from left-distributivity and
+          commutativity.\<close>
   proof (rule ring_axioms.intro)
     fix x y z
     assume R: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
@@ -312,7 +312,7 @@
   "cring R" by (rule cring_axioms)
 
 
-subsubsection {* Normaliser for Rings *}
+subsubsection \<open>Normaliser for Rings\<close>
 
 lemma (in abelian_group) r_neg2:
   "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus> (\<ominus> x \<oplus> y) = y"
@@ -335,9 +335,9 @@
 
 context ring begin
 
-text {* 
+text \<open>
   The following proofs are from Jacobson, Basic Algebra I, pp.~88--89.
-*}
+\<close>
 
 sublocale semiring
 proof -
@@ -387,20 +387,20 @@
   "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<ominus> y = x \<oplus> \<ominus> y"
   by (simp only: a_minus_def)
 
-text {* Setup algebra method:
-  compute distributive normal form in locale contexts *}
+text \<open>Setup algebra method:
+  compute distributive normal form in locale contexts\<close>
 
 ML_file "ringsimp.ML"
 
-attribute_setup algebra = {*
+attribute_setup algebra = \<open>
   Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon || Scan.succeed true)
     -- Scan.lift Args.name -- Scan.repeat Args.term
     >> (fn ((b, n), ts) => if b then Ringsimp.add_struct (n, ts) else Ringsimp.del_struct (n, ts))
-*} "theorems controlling algebra method"
+\<close> "theorems controlling algebra method"
 
-method_setup algebra = {*
+method_setup algebra = \<open>
   Scan.succeed (SIMPLE_METHOD' o Ringsimp.algebra_tac)
-*} "normalisation of algebraic structure"
+\<close> "normalisation of algebraic structure"
 
 lemmas (in semiring) semiring_simprules
   [algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
@@ -463,7 +463,7 @@
 
 end
 
-text {* Two examples for use of method algebra *}
+text \<open>Two examples for use of method algebra\<close>
 
 lemma
   fixes R (structure) and S (structure)
@@ -487,7 +487,7 @@
 qed
 
 
-subsubsection {* Sums over Finite Sets *}
+subsubsection \<open>Sums over Finite Sets\<close>
 
 lemma (in semiring) finsum_ldistr:
   "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
@@ -508,7 +508,7 @@
 qed
 
 
-subsection {* Integral Domains *}
+subsection \<open>Integral Domains\<close>
 
 context "domain" begin
 
@@ -554,10 +554,10 @@
 end
 
 
-subsection {* Fields *}
+subsection \<open>Fields\<close>
 
-text {* Field would not need to be derived from domain, the properties
-  for domain follow from the assumptions of field *}
+text \<open>Field would not need to be derived from domain, the properties
+  for domain follow from the assumptions of field\<close>
 lemma (in cring) cring_fieldI:
   assumes field_Units: "Units R = carrier R - {\<zero>}"
   shows "field R"
@@ -585,7 +585,7 @@
   qed
 qed (rule field_Units)
 
-text {* Another variant to show that something is a field *}
+text \<open>Another variant to show that something is a field\<close>
 lemma (in cring) cring_fieldI2:
   assumes notzero: "\<zero> \<noteq> \<one>"
   and invex: "\<And>a. \<lbrakk>a \<in> carrier R; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>b\<in>carrier R. a \<otimes> b = \<one>"
@@ -604,7 +604,7 @@
 qed
 
 
-subsection {* Morphisms *}
+subsection \<open>Morphisms\<close>
 
 definition
   ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set"
diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/RingHom.thy
--- a/src/HOL/Algebra/RingHom.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/RingHom.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -6,9 +6,9 @@
 imports Ideal
 begin
 
-section {* Homomorphisms of Non-Commutative Rings *}
+section \<open>Homomorphisms of Non-Commutative Rings\<close>
 
-text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *}
+text \<open>Lifting existing lemmas in a @{text ring_hom_ring} locale\<close>
 locale ring_hom_ring = R: ring R + S: ring S
     for R (structure) and S (structure) +
   fixes h
@@ -100,7 +100,7 @@
 qed
 
 
-subsection {* The Kernel of a Ring Homomorphism *}
+subsection \<open>The Kernel of a Ring Homomorphism\<close>
 
 --"the kernel of a ring homomorphism is an ideal"
 lemma (in ring_hom_ring) kernel_is_ideal:
@@ -111,15 +111,15 @@
  apply (unfold a_kernel_def', simp+)
 done
 
-text {* Elements of the kernel are mapped to zero *}
+text \<open>Elements of the kernel are mapped to zero\<close>
 lemma (in abelian_group_hom) kernel_zero [simp]:
   "i \<in> a_kernel R S h \<Longrightarrow> h i = \<zero>\<^bsub>S\<^esub>"
 by (simp add: a_kernel_defs)
 
 
-subsection {* Cosets *}
+subsection \<open>Cosets\<close>
 
-text {* Cosets of the kernel correspond to the elements of the image of the homomorphism *}
+text \<open>Cosets of the kernel correspond to the elements of the image of the homomorphism\<close>
 lemma (in ring_hom_ring) rcos_imp_homeq:
   assumes acarr: "a \<in> carrier R"
       and xrcos: "x \<in> a_kernel R S h +> a"
diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/Sylow.thy
--- a/src/HOL/Algebra/Sylow.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/Sylow.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -6,11 +6,11 @@
 imports Coset Exponent
 begin
 
-text {*
+text \<open>
   See also @{cite "Kammueller-Paulson:1999"}.
-*}
+\<close>
 
-text{*The combinatorial argument is in theory Exponent*}
+text\<open>The combinatorial argument is in theory Exponent\<close>
 
 locale sylow = group +
   fixes p and a and m and calM and RelM
@@ -49,7 +49,7 @@
 done
 
 
-subsection{*Main Part of the Proof*}
+subsection\<open>Main Part of the Proof\<close>
 
 locale sylow_central = sylow +
   fixes H and M1 and M
@@ -107,7 +107,7 @@
   qed
 
 
-subsection{*Discharging the Assumptions of @{text sylow_central}*}
+subsection\<open>Discharging the Assumptions of @{text sylow_central}\<close>
 
 lemma (in sylow) EmptyNotInEquivSet: "{} \<notin> calM // RelM"
 by (blast elim!: quotientE dest: RelM_equiv [THEN equiv_class_self])
@@ -155,7 +155,7 @@
 done
 
 
-subsubsection{*Introduction and Destruct Rules for @{term H}*}
+subsubsection\<open>Introduction and Destruct Rules for @{term H}\<close>
 
 lemma (in sylow_central) H_I: "[|g \<in> carrier G; M1 #> g = M1|] ==> g \<in> H"
 by (simp add: H_def)
@@ -216,10 +216,10 @@
 done
 
 
-subsection{*Equal Cardinalities of @{term M} and the Set of Cosets*}
+subsection\<open>Equal Cardinalities of @{term M} and the Set of Cosets\<close>
 
-text{*Injections between @{term M} and @{term "rcosets\<^bsub>G\<^esub> H"} show that
- their cardinalities are equal.*}
+text\<open>Injections between @{term M} and @{term "rcosets\<^bsub>G\<^esub> H"} show that
+ their cardinalities are equal.\<close>
 
 lemma ElemClassEquiv:
      "[| equiv A r; C \<in> A // r |] ==> \<forall>x \<in> C. \<forall>y \<in> C. (x,y)\<in>r"
@@ -259,7 +259,7 @@
 done
 
 
-subsubsection{*The Opposite Injection*}
+subsubsection\<open>The Opposite Injection\<close>
 
 lemma (in sylow_central) H_elem_map:
      "H1 \<in> rcosets H ==> \<exists>g. g \<in> carrier G & H #> g = H1"
@@ -278,7 +278,7 @@
             intro!: M1_in_M in_quotient_imp_closed [OF RelM_equiv M_in_quot _  M1_RelM_rcosetGM1g])
 done
 
-text{*close to a duplicate of @{text inj_M_GmodH}*}
+text\<open>close to a duplicate of @{text inj_M_GmodH}\<close>
 lemma (in sylow_central) inj_GmodH_M:
      "\<exists>g \<in> rcosets H\<rightarrow>M. inj_on g (rcosets H)"
 apply (rule bexI)
@@ -340,14 +340,14 @@
 apply (simp add: sylow_central_def sylow_central_axioms_def sylow_axioms calM_def RelM_def)
 done
 
-text{*Needed because the locale's automatic definition refers to
+text\<open>Needed because the locale's automatic definition refers to
    @{term "semigroup G"} and @{term "group_axioms G"} rather than
-  simply to @{term "group G"}.*}
+  simply to @{term "group G"}.\<close>
 lemma sylow_eq: "sylow G p a m = (group G & sylow_axioms G p a m)"
 by (simp add: sylow_def group_def)
 
 
-subsection {* Sylow's Theorem *}
+subsection \<open>Sylow's Theorem\<close>
 
 theorem sylow_thm:
      "[| prime p;  group(G);  order(G) = (p^a) * m; finite (carrier G)|]
diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -9,9 +9,9 @@
 imports Module RingHom
 begin
 
-section {* Univariate Polynomials *}
+section \<open>Univariate Polynomials\<close>
 
-text {*
+text \<open>
   Polynomials are formalised as modules with additional operations for
   extracting coefficients from polynomials and for obtaining monomials
   from coefficients and exponents (record @{text "up_ring"}).  The
@@ -21,14 +21,14 @@
   formalisation of polynomials in the PhD thesis @{cite "Ballarin:1999"},
   which was implemented with axiomatic type classes.  This was later
   ported to Locales.
-*}
+\<close>
 
 
-subsection {* The Constructor for Univariate Polynomials *}
+subsection \<open>The Constructor for Univariate Polynomials\<close>
 
-text {*
+text \<open>
   Functions with finite support.
-*}
+\<close>
 
 locale bound =
   fixes z :: 'a
@@ -67,9 +67,9 @@
    monom = (%a:carrier R. %n i. if i=n then a else \<zero>\<^bsub>R\<^esub>),
    coeff = (%p:up R. %n. p n)\<rparr>"
 
-text {*
+text \<open>
   Properties of the set of polynomials @{term up}.
-*}
+\<close>
 
 lemma mem_upI [intro]:
   "[| !!n. f n \<in> carrier R; EX n. bound (zero R) n f |] ==> f \<in> up R"
@@ -168,7 +168,7 @@
 end
 
 
-subsection {* Effect of Operations on Coefficients *}
+subsection \<open>Effect of Operations on Coefficients\<close>
 
 locale UP =
   fixes R (structure) and P (structure)
@@ -189,7 +189,7 @@
 context UP
 begin
 
-text {*Temporarily declare @{thm P_def} as simp rule.*}
+text \<open>Temporarily declare @{thm P_def} as simp rule.\<close>
 
 declare P_def [simp]
 
@@ -240,12 +240,12 @@
 end
 
 
-subsection {* Polynomials Form a Ring. *}
+subsection \<open>Polynomials Form a Ring.\<close>
 
 context UP_ring
 begin
 
-text {* Operations are closed over @{term P}. *}
+text \<open>Operations are closed over @{term P}.\<close>
 
 lemma UP_mult_closed [simp]:
   "[| 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)
@@ -269,7 +269,7 @@
 
 declare (in UP) P_def [simp del]
 
-text {* Algebraic ring properties *}
+text \<open>Algebraic ring properties\<close>
 
 context UP_ring
 begin
@@ -398,7 +398,7 @@
 end
 
 
-subsection {* Polynomials Form a Commutative Ring. *}
+subsection \<open>Polynomials Form a Commutative Ring.\<close>
 
 context UP_cring
 begin
@@ -428,7 +428,7 @@
 qed (simp_all add: R1 R2)
 
 
-subsection {*Polynomials over a commutative ring for a commutative ring*}
+subsection \<open>Polynomials over a commutative ring for a commutative ring\<close>
 
 theorem UP_cring:
   "cring P" using UP_ring unfolding cring_def by (auto intro!: comm_monoidI UP_m_assoc UP_m_comm)
@@ -461,7 +461,7 @@
 sublocale UP_cring < P: cring P using UP_cring .
 
 
-subsection {* Polynomials Form an Algebra *}
+subsection \<open>Polynomials Form an Algebra\<close>
 
 context UP_ring
 begin
@@ -496,9 +496,9 @@
 
 end
 
-text {*
+text \<open>
   Interpretation of lemmas from @{term algebra}.
-*}
+\<close>
 
 lemma (in cring) cring:
   "cring R" ..
@@ -510,7 +510,7 @@
 sublocale UP_cring < algebra R P using UP_algebra .
 
 
-subsection {* Further Lemmas Involving Monomials *}
+subsection \<open>Further Lemmas Involving Monomials\<close>
 
 context UP_ring
 begin
@@ -637,8 +637,8 @@
   }
 qed
 
-text{*The following corollary follows from lemmas @{thm "monom_one_Suc"} 
-  and @{thm "monom_one_Suc2"}, and is trivial in @{term UP_cring}*}
+text\<open>The following corollary follows from lemmas @{thm "monom_one_Suc"} 
+  and @{thm "monom_one_Suc2"}, and is trivial in @{term UP_cring}\<close>
 
 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"
   unfolding monom_one_Suc [symmetric] monom_one_Suc2 [symmetric] ..
@@ -709,7 +709,7 @@
 end
 
 
-subsection {* The Degree Function *}
+subsection \<open>The Degree Function\<close>
 
 definition
   deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
@@ -743,19 +743,19 @@
   assumes "deg R p < m" and "p \<in> carrier P"
   shows "coeff P p m = \<zero>"
 proof -
-  from `p \<in> carrier P` obtain n where "bound \<zero> n (coeff P p)"
+  from \<open>p \<in> carrier P\<close> obtain n where "bound \<zero> n (coeff P p)"
     by (auto simp add: UP_def P_def)
   then have "bound \<zero> (deg R p) (coeff P p)"
     by (auto simp: deg_def P_def dest: LeastI)
-  from this and `deg R p < m` show ?thesis ..
+  from this and \<open>deg R p < m\<close> show ?thesis ..
 qed
 
 lemma deg_belowI:
   assumes non_zero: "n ~= 0 ==> coeff P p n ~= \<zero>"
     and R: "p \<in> carrier P"
   shows "n <= deg R p"
--- {* Logically, this is a slightly stronger version of
-   @{thm [source] deg_aboveD} *}
+-- \<open>Logically, this is a slightly stronger version of
+   @{thm [source] deg_aboveD}\<close>
 proof (cases "n=0")
   case True then show ?thesis by simp
 next
@@ -814,7 +814,7 @@
       !!n. n ~= 0 ==> coeff P p n ~= \<zero>; p \<in> carrier P |] ==> deg R p = n"
 by (fast intro: le_antisym deg_aboveI deg_belowI)
 
-text {* Degree and polynomial operations *}
+text \<open>Degree and polynomial operations\<close>
 
 lemma deg_add [simp]:
   "p \<in> carrier P \<Longrightarrow> q \<in> carrier P \<Longrightarrow>
@@ -863,8 +863,8 @@
       inj_on_iff [OF R.a_inv_inj, of _ "\<zero>", simplified] R)
 qed
 
-text{*The following lemma is later \emph{overwritten} by the most
-  specific one for domains, @{text deg_smult}.*}
+text\<open>The following lemma is later \emph{overwritten} by the most
+  specific one for domains, @{text deg_smult}.\<close>
 
 lemma deg_smult_ring [simp]:
   "[| a \<in> carrier R; p \<in> carrier P |] ==>
@@ -949,7 +949,7 @@
 
 end
 
-text{*The following lemmas also can be lifted to @{term UP_ring}.*}
+text\<open>The following lemmas also can be lifted to @{term UP_ring}.\<close>
 
 context UP_ring
 begin
@@ -1013,7 +1013,7 @@
 end
 
 
-subsection {* Polynomials over Integral Domains *}
+subsection \<open>Polynomials over Integral Domains\<close>
 
 lemma domainI:
   assumes cring: "cring R"
@@ -1071,15 +1071,15 @@
 
 end
 
-text {*
+text \<open>
   Interpretation of theorems from @{term domain}.
-*}
+\<close>
 
 sublocale UP_domain < "domain" P
   by intro_locales (rule domain.axioms UP_domain)+
 
 
-subsection {* The Evaluation Homomorphism and Universal Property*}
+subsection \<open>The Evaluation Homomorphism and Universal Property\<close>
 
 (* alternative congruence rule (possibly more efficient)
 lemma (in abelian_monoid) finsum_cong2:
@@ -1192,7 +1192,7 @@
 
 end
 
-text {* The universal property of the polynomial ring *}
+text \<open>The universal property of the polynomial ring\<close>
 
 locale UP_pre_univ_prop = ring_hom_cring + UP_cring
 
@@ -1203,9 +1203,9 @@
   assumes indet_img_carrier [simp, intro]: "s \<in> carrier S"
   defines Eval_def: "Eval == eval R S h s"
 
-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}.*}
-text{*JE: I was considering using it in @{text eval_ring_hom}, but that property does not hold for non commutative rings, so 
-  maybe it is not that necessary.*}
+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>
+text\<open>JE: I was considering using it in @{text eval_ring_hom}, but that property does not hold for non commutative rings, so 
+  maybe it is not that necessary.\<close>
 
 lemma (in ring_hom_ring) hom_finsum [simp]:
   "f \<in> A -> carrier R ==>
@@ -1296,18 +1296,18 @@
   qed
 qed
 
-text {*
+text \<open>
   The following lemma could be proved in @{text UP_cring} with the additional
-  assumption that @{text h} is closed. *}
+  assumption that @{text h} is closed.\<close>
 
 lemma (in UP_pre_univ_prop) eval_const:
   "[| s \<in> carrier S; r \<in> carrier R |] ==> eval R S h s (monom P r 0) = h r"
   by (simp only: eval_on_carrier monom_closed) simp
 
-text {* Further properties of the evaluation homomorphism. *}
+text \<open>Further properties of the evaluation homomorphism.\<close>
 
-text {* The following proof is complicated by the fact that in arbitrary
-  rings one might have @{term "one R = zero R"}. *}
+text \<open>The following proof is complicated by the fact that in arbitrary
+  rings one might have @{term "one R = zero R"}.\<close>
 
 (* TODO: simplify by cases "one R = zero R" *)
 
@@ -1336,7 +1336,7 @@
 
 end
 
-text {* Interpretation of ring homomorphism lemmas. *}
+text \<open>Interpretation of ring homomorphism lemmas.\<close>
 
 sublocale UP_univ_prop < ring_hom_cring P S Eval
   unfolding Eval_def
@@ -1442,7 +1442,7 @@
 
 end
 
-text{*JE: The following lemma was added by me; it might be even lifted to a simpler locale*}
+text\<open>JE: The following lemma was added by me; it might be even lifted to a simpler locale\<close>
 
 context monoid
 begin
@@ -1461,7 +1461,7 @@
   using lcoeff_nonzero [OF p_not_zero p_in_R] .
 
 
-subsection{*The long division algorithm: some previous facts.*}
+subsection\<open>The long division algorithm: some previous facts.\<close>
 
 lemma coeff_minus [simp]:
   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" 
@@ -1538,7 +1538,7 @@
 end
 
 
-subsection {* The long division proof for commutative rings *}
+subsection \<open>The long division proof for commutative rings\<close>
 
 context UP_cring
 begin
@@ -1547,7 +1547,7 @@
   shows "\<exists> x y z. Pred x y z"
   using exist by blast
 
-text {* Jacobson's Theorem 2.14 *}
+text \<open>Jacobson's Theorem 2.14\<close>
 
 lemma long_div_theorem: 
   assumes g_in_P [simp]: "g \<in> carrier P" and f_in_P [simp]: "f \<in> carrier P"
@@ -1648,7 +1648,7 @@
 end
 
 
-text {*The remainder theorem as corollary of the long division theorem.*}
+text \<open>The remainder theorem as corollary of the long division theorem.\<close>
 
 context UP_cring
 begin
@@ -1797,7 +1797,7 @@
 end
 
 
-subsection {* Sample Application of Evaluation Homomorphism *}
+subsection \<open>Sample Application of Evaluation Homomorphism\<close>
 
 lemma UP_pre_univ_propI:
   assumes "cring R"
@@ -1820,11 +1820,11 @@
   "UP_pre_univ_prop INTEG INTEG id"
   by (fast intro: UP_pre_univ_propI INTEG_cring id_ring_hom)
 
-text {*
+text \<open>
   Interpretation now enables to import all theorems and lemmas
   valid in the context of homomorphisms between @{term INTEG} and @{term
   "UP INTEG"} globally.
-*}
+\<close>
 
 interpretation INTEG: UP_pre_univ_prop INTEG INTEG id "UP INTEG"
   using INTEG_id_eval by simp_all
diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/BijectionRel.thy
--- a/src/HOL/Old_Number_Theory/BijectionRel.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/BijectionRel.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -3,18 +3,18 @@
     Copyright   2000  University of Cambridge
 *)
 
-section {* Bijections between sets *}
+section \<open>Bijections between sets\<close>
 
 theory BijectionRel
 imports Main
 begin
 
-text {*
+text \<open>
   Inductive definitions of bijections between two different sets and
   between the same set.  Theorem for relating the two definitions.
 
   \bigskip
-*}
+\<close>
 
 inductive_set
   bijR :: "('a => 'b => bool) => ('a set * 'b set) set"
@@ -24,10 +24,10 @@
 | insert: "P a b ==> a \<notin> A ==> b \<notin> B ==> (A, B) \<in> bijR P
     ==> (insert a A, insert b B) \<in> bijR P"
 
-text {*
+text \<open>
   Add extra condition to @{term insert}: @{term "\<forall>b \<in> B. \<not> P a b"}
   (and similar for @{term A}).
-*}
+\<close>
 
 definition
   bijP :: "('a => 'a => bool) => 'a set => bool" where
@@ -51,7 +51,7 @@
     ==> insert a (insert b A) \<in> bijER P"
 
 
-text {* \medskip @{term bijR} *}
+text \<open>\medskip @{term bijR}\<close>
 
 lemma fin_bijRl: "(A, B) \<in> bijR P ==> finite A"
   apply (erule bijR.induct)
@@ -100,7 +100,7 @@
   done
 
 
-text {* \medskip @{term bijER} *}
+text \<open>\medskip @{term bijER}\<close>
 
 lemma fin_bijER: "A \<in> bijER P ==> finite A"
   apply (erule bijER.induct)
diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/Chinese.thy
--- a/src/HOL/Old_Number_Theory/Chinese.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Chinese.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -3,22 +3,22 @@
     Copyright   2000  University of Cambridge
 *)
 
-section {* The Chinese Remainder Theorem *}
+section \<open>The Chinese Remainder Theorem\<close>
 
 theory Chinese 
 imports IntPrimes
 begin
 
-text {*
+text \<open>
   The Chinese Remainder Theorem for an arbitrary finite number of
   equations.  (The one-equation case is included in theory @{text
   IntPrimes}.  Uses functions for indexing.\footnote{Maybe @{term
   funprod} and @{term funsum} should be based on general @{term fold}
   on indices?}
-*}
+\<close>
 
 
-subsection {* Definitions *}
+subsection \<open>Definitions\<close>
 
 primrec funprod :: "(nat => int) => nat => nat => int"
 where
@@ -65,7 +65,7 @@
   "x_sol n kf bf mf = funsum (\<lambda>i. xilin_sol i n kf bf mf * mhf mf n i) 0 n"
 
 
-text {* \medskip @{term funprod} and @{term funsum} *}
+text \<open>\medskip @{term funprod} and @{term funsum}\<close>
 
 lemma funprod_pos: "(\<forall>i. i \<le> n --> 0 < mf i) ==> 0 < funprod mf 0 n"
 by (induct n) auto
@@ -126,7 +126,7 @@
   done
 
 
-subsection {* Chinese: uniqueness *}
+subsection \<open>Chinese: uniqueness\<close>
 
 lemma zcong_funprod_aux:
   "m_cond n mf ==> km_cond n kf mf
@@ -160,17 +160,17 @@
   done
 
 
-subsection {* Chinese: existence *}
+subsection \<open>Chinese: existence\<close>
 
 lemma unique_xi_sol:
   "0 < n ==> i \<le> n ==> m_cond n mf ==> km_cond n kf mf
     ==> \<exists>!x. 0 \<le> x \<and> x < mf i \<and> [kf i * mhf mf n i * x = bf i] (mod mf i)"
   apply (rule zcong_lineq_unique)
-   apply (tactic {* stac @{context} @{thm zgcd_zmult_cancel} 2 *})
+   apply (tactic \<open>stac @{context} @{thm zgcd_zmult_cancel} 2\<close>)
     apply (unfold m_cond_def km_cond_def mhf_def)
     apply (simp_all (no_asm_simp))
   apply safe
-    apply (tactic {* stac @{context} @{thm zgcd_zmult_cancel} 3 *})
+    apply (tactic \<open>stac @{context} @{thm zgcd_zmult_cancel} 3\<close>)
      apply (rule_tac [!] funprod_zgcd)
      apply safe
      apply simp_all
@@ -216,7 +216,7 @@
   done
 
 
-subsection {* Chinese *}
+subsection \<open>Chinese\<close>
 
 lemma chinese_remainder:
   "0 < n ==> m_cond n mf ==> km_cond n kf mf
@@ -228,19 +228,19 @@
   apply (rule_tac x = "x_sol n kf bf mf mod funprod mf 0 n" in exI)
   apply (unfold lincong_sol_def)
   apply safe
-    apply (tactic {* stac @{context} @{thm zcong_zmod} 3 *})
-    apply (tactic {* stac @{context} @{thm mod_mult_eq} 3 *})
-    apply (tactic {* stac @{context} @{thm mod_mod_cancel} 3 *})
-      apply (tactic {* stac @{context} @{thm x_sol_lin} 4 *})
-        apply (tactic {* stac @{context} (@{thm mod_mult_eq} RS sym) 6 *})
-        apply (tactic {* stac @{context} (@{thm zcong_zmod} RS sym) 6 *})
+    apply (tactic \<open>stac @{context} @{thm zcong_zmod} 3\<close>)
+    apply (tactic \<open>stac @{context} @{thm mod_mult_eq} 3\<close>)
+    apply (tactic \<open>stac @{context} @{thm mod_mod_cancel} 3\<close>)
+      apply (tactic \<open>stac @{context} @{thm x_sol_lin} 4\<close>)
+        apply (tactic \<open>stac @{context} (@{thm mod_mult_eq} RS sym) 6\<close>)
+        apply (tactic \<open>stac @{context} (@{thm zcong_zmod} RS sym) 6\<close>)
         apply (subgoal_tac [6]
           "0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
           \<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
          prefer 6
          apply (simp add: ac_simps)
         apply (unfold xilin_sol_def)
-        apply (tactic {* asm_simp_tac @{context} 6 *})
+        apply (tactic \<open>asm_simp_tac @{context} 6\<close>)
         apply (rule_tac [6] ex1_implies_ex [THEN someI_ex])
         apply (rule_tac [6] unique_xi_sol)
            apply (rule_tac [3] funprod_zdvd)
diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/Euler.thy
--- a/src/HOL/Old_Number_Theory/Euler.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Euler.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -2,7 +2,7 @@
     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
 *)
 
-section {* Euler's criterion *}
+section \<open>Euler's criterion\<close>
 
 theory Euler
 imports Residues EvenOdd
@@ -15,7 +15,7 @@
   where "SetS a p = MultInvPair a p ` SRStar p"
 
 
-subsection {* Property for MultInvPair *}
+subsection \<open>Property for MultInvPair\<close>
 
 lemma MultInvPair_prop1a:
   "[| zprime p; 2 < p; ~([a = 0](mod p));
@@ -89,7 +89,7 @@
   done
 
 
-subsection {* Properties of SetS *}
+subsection \<open>Properties of SetS\<close>
 
 lemma SetS_finite: "2 < p ==> finite (SetS a p)"
   by (auto simp add: SetS_def SRStar_finite [of p])
@@ -223,14 +223,14 @@
   apply (auto simp add: Union_SetS_setprod_prop2)
   done
 
-text {* \medskip Prove the first part of Euler's Criterion: *}
+text \<open>\medskip Prove the first part of Euler's Criterion:\<close>
 
 lemma Euler_part1: "[| 2 < p; zprime p; ~([x = 0](mod p)); 
     ~(QuadRes p x) |] ==> 
       [x^(nat (((p) - 1) div 2)) = -1](mod p)"
   by (metis Wilson_Russ zcong_sym zcong_trans zfact_prop)
 
-text {* \medskip Prove another part of Euler Criterion: *}
+text \<open>\medskip Prove another part of Euler Criterion:\<close>
 
 lemma aux_1: "0 < p ==> (a::int) ^ nat (p) = a * a ^ (nat (p) - 1)"
 proof -
@@ -251,7 +251,7 @@
     by (auto simp add: zEven_def zOdd_def)
   then have aux_1: "2 * ((p - 1) div 2) = (p - 1)"
     by (auto simp add: even_div_2_prop2)
-  with `2 < p` have "1 < (p - 1)"
+  with \<open>2 < p\<close> have "1 < (p - 1)"
     by auto
   then have " 1 < (2 * ((p - 1) div 2))"
     by (auto simp add: aux_1)
@@ -268,7 +268,7 @@
   apply (frule zcong_zmult_prop1, auto)
   done
 
-text {* \medskip Prove the final part of Euler's Criterion: *}
+text \<open>\medskip Prove the final part of Euler's Criterion:\<close>
 
 lemma aux__1: "[| ~([x = 0] (mod p)); [y\<^sup>2 = x] (mod p)|] ==> ~(p dvd y)"
   by (metis dvdI power2_eq_square zcong_sym zcong_trans zcong_zero_equiv_div dvd_trans)
@@ -291,7 +291,7 @@
   done
 
 
-text {* \medskip Finally show Euler's Criterion: *}
+text \<open>\medskip Finally show Euler's Criterion:\<close>
 
 theorem Euler_Criterion: "[| 2 < p; zprime p |] ==> [(Legendre a p) =
     a^(nat (((p) - 1) div 2))] (mod p)"
diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/EulerFermat.thy
--- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -3,20 +3,20 @@
     Copyright   2000  University of Cambridge
 *)
 
-section {* Fermat's Little Theorem extended to Euler's Totient function *}
+section \<open>Fermat's Little Theorem extended to Euler's Totient function\<close>
 
 theory EulerFermat
 imports BijectionRel IntFact
 begin
 
-text {*
+text \<open>
   Fermat's Little Theorem extended to Euler's Totient function. More
   abstract approach than Boyer-Moore (which seems necessary to achieve
   the extended version).
-*}
+\<close>
 
 
-subsection {* Definitions and lemmas *}
+subsection \<open>Definitions and lemmas\<close>
 
 inductive_set RsetR :: "int => int set set" for m :: int
 where
@@ -54,11 +54,11 @@
   where "zcongm m = (\<lambda>a b. zcong a b m)"
 
 lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)"
-  -- {* LCP: not sure why this lemma is needed now *}
+  -- \<open>LCP: not sure why this lemma is needed now\<close>
   by (auto simp add: abs_if)
 
 
-text {* \medskip @{text norRRset} *}
+text \<open>\medskip @{text norRRset}\<close>
 
 declare BnorRset.simps [simp del]
 
@@ -146,7 +146,7 @@
   done
 
 
-text {* \medskip @{term noXRRset} *}
+text \<open>\medskip @{term noXRRset}\<close>
 
 lemma RRset_gcd [rule_format]:
     "is_RRset A m ==> a \<in> A --> zgcd a m = 1"
@@ -249,7 +249,7 @@
       \<Prod>(BnorRset a m) * x^card (BnorRset a m)"
   apply (induct a m rule: BnorRset_induct)
    prefer 2
-   apply (simplesubst BnorRset.simps)  --{*multiple redexes*}
+   apply (simplesubst BnorRset.simps)  --\<open>multiple redexes\<close>
    apply (unfold Let_def, auto)
   apply (simp add: Bnor_fin Bnor_mem_zle_swap)
   apply (subst setprod.insert)
@@ -259,7 +259,7 @@
   done
 
 
-subsection {* Fermat *}
+subsection \<open>Fermat\<close>
 
 lemma bijzcong_zcong_prod:
     "(A, B) \<in> bijR (zcongm m) ==> [\<Prod>A = \<Prod>B] (mod m)"
diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/EvenOdd.thy
--- a/src/HOL/Old_Number_Theory/EvenOdd.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/EvenOdd.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -2,7 +2,7 @@
     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
 *)
 
-section {*Parity: Even and Odd Integers*}
+section \<open>Parity: Even and Odd Integers\<close>
 
 theory EvenOdd
 imports Int2
@@ -14,7 +14,7 @@
 definition zEven :: "int set"
   where "zEven = {x. \<exists>k. x = 2 * k}"
 
-subsection {* Some useful properties about even and odd *}
+subsection \<open>Some useful properties about even and odd\<close>
 
 lemma zOddI [intro?]: "x = 2 * k + 1 \<Longrightarrow> x \<in> zOdd"
   and zOddE [elim?]: "x \<in> zOdd \<Longrightarrow> (!!k. x = 2 * k + 1 \<Longrightarrow> C) \<Longrightarrow> C"
@@ -167,11 +167,11 @@
 lemma neg_one_even_power: "[| x \<in> zEven; 0 \<le> x |] ==> (-1::int)^(nat x) = 1"
 proof -
   assume "x \<in> zEven" and "0 \<le> x"
-  from `x \<in> zEven` obtain a where "x = 2 * a" ..
-  with `0 \<le> x` have "0 \<le> a" by simp
-  from `0 \<le> x` and `x = 2 * a` have "nat x = nat (2 * a)"
+  from \<open>x \<in> zEven\<close> obtain a where "x = 2 * a" ..
+  with \<open>0 \<le> x\<close> have "0 \<le> a" by simp
+  from \<open>0 \<le> x\<close> and \<open>x = 2 * a\<close> have "nat x = nat (2 * a)"
     by simp
-  also from `x = 2 * a` have "nat (2 * a) = 2 * nat a"
+  also from \<open>x = 2 * a\<close> have "nat (2 * a) = 2 * nat a"
     by (simp add: nat_mult_distrib)
   finally have "(-1::int)^nat x = (-1)^(2 * nat a)"
     by simp
@@ -186,9 +186,9 @@
 lemma neg_one_odd_power: "[| x \<in> zOdd; 0 \<le> x |] ==> (-1::int)^(nat x) = -1"
 proof -
   assume "x \<in> zOdd" and "0 \<le> x"
-  from `x \<in> zOdd` obtain a where "x = 2 * a + 1" ..
-  with `0 \<le> x` have a: "0 \<le> a" by simp
-  with `0 \<le> x` and `x = 2 * a + 1` have "nat x = nat (2 * a + 1)"
+  from \<open>x \<in> zOdd\<close> obtain a where "x = 2 * a + 1" ..
+  with \<open>0 \<le> x\<close> have a: "0 \<le> a" by simp
+  with \<open>0 \<le> x\<close> and \<open>x = 2 * a + 1\<close> have "nat x = nat (2 * a + 1)"
     by simp
   also from a have "nat (2 * a + 1) = 2 * nat a + 1"
     by (auto simp add: nat_mult_distrib nat_add_distrib)
@@ -214,8 +214,8 @@
 lemma even_div_2_l: "[| y \<in> zEven; x < y |] ==> x div 2 < y div 2"
 proof -
   assume "y \<in> zEven" and "x < y"
-  from `y \<in> zEven` obtain k where k: "y = 2 * k" ..
-  with `x < y` have "x < 2 * k" by simp
+  from \<open>y \<in> zEven\<close> obtain k where k: "y = 2 * k" ..
+  with \<open>x < y\<close> have "x < 2 * k" by simp
   then have "x div 2 < k" by (auto simp add: div_prop1)
   also have "k = (2 * k) div 2" by simp
   finally have "x div 2 < 2 * k div 2" by simp
diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/Factorization.thy
--- a/src/HOL/Old_Number_Theory/Factorization.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Factorization.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -3,14 +3,14 @@
     Copyright   2000  University of Cambridge
 *)
 
-section {* Fundamental Theorem of Arithmetic (unique factorization into primes) *}
+section \<open>Fundamental Theorem of Arithmetic (unique factorization into primes)\<close>
 
 theory Factorization
 imports Primes "~~/src/HOL/Library/Permutation"
 begin
 
 
-subsection {* Definitions *}
+subsection \<open>Definitions\<close>
 
 definition primel :: "nat list => bool"
   where "primel xs = (\<forall>p \<in> set xs. prime p)"
@@ -36,7 +36,7 @@
 | "sort (x # xs) = oinsert x (sort xs)"
 
 
-subsection {* Arithmetic *}
+subsection \<open>Arithmetic\<close>
 
 lemma one_less_m: "(m::nat) \<noteq> m * k ==> m \<noteq> Suc 0 ==> Suc 0 < m"
   apply (cases m)
@@ -64,7 +64,7 @@
   done
 
 
-subsection {* Prime list and product *}
+subsection \<open>Prime list and product\<close>
 
 lemma prod_append: "prod (xs @ ys) = prod xs * prod ys"
   apply (induct xs)
@@ -137,7 +137,7 @@
   done
 
 
-subsection {* Sorting *}
+subsection \<open>Sorting\<close>
 
 lemma nondec_oinsert: "nondec xs \<Longrightarrow> nondec (oinsert x xs)"
   apply (induct xs)
@@ -174,7 +174,7 @@
   done
 
 
-subsection {* Permutation *}
+subsection \<open>Permutation\<close>
 
 lemma perm_primel [rule_format]: "xs <~~> ys ==> primel xs --> primel ys"
   apply (unfold primel_def)
@@ -212,7 +212,7 @@
   done
 
 
-subsection {* Existence *}
+subsection \<open>Existence\<close>
 
 lemma ex_nondec_lemma:
     "primel xs ==> \<exists>ys. primel ys \<and> nondec ys \<and> prod ys = prod xs"
@@ -250,7 +250,7 @@
   done
 
 
-subsection {* Uniqueness *}
+subsection \<open>Uniqueness\<close>
 
 lemma prime_dvd_mult_list [rule_format]:
     "prime p ==> p dvd (prod xs) --> (\<exists>m. m:set xs \<and> p dvd m)"
diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/Fib.thy
--- a/src/HOL/Old_Number_Theory/Fib.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Fib.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -3,19 +3,19 @@
     Copyright   1997  University of Cambridge
 *)
 
-section {* The Fibonacci function *}
+section \<open>The Fibonacci function\<close>
 
 theory Fib
 imports Primes
 begin
 
-text {*
+text \<open>
   Fibonacci numbers: proofs of laws taken from:
   R. L. Graham, D. E. Knuth, O. Patashnik.  Concrete Mathematics.
   (Addison-Wesley, 1989)
 
   \bigskip
-*}
+\<close>
 
 fun fib :: "nat \<Rightarrow> nat"
 where
@@ -23,21 +23,21 @@
 | "fib (Suc 0) = 1"
 | fib_2: "fib (Suc (Suc n)) = fib n + fib (Suc n)"
 
-text {*
+text \<open>
   \medskip The difficulty in these proofs is to ensure that the
   induction hypotheses are applied before the definition of @{term
   fib}.  Towards this end, the @{term fib} equations are not declared
   to the Simplifier and are applied very selectively at first.
-*}
+\<close>
 
-text{*We disable @{text fib.fib_2fib_2} for simplification ...*}
+text\<open>We disable @{text fib.fib_2fib_2} for simplification ...\<close>
 declare fib_2 [simp del]
 
-text{*...then prove a version that has a more restrictive pattern.*}
+text\<open>...then prove a version that has a more restrictive pattern.\<close>
 lemma fib_Suc3: "fib (Suc (Suc (Suc n))) = fib (Suc n) + fib (Suc (Suc n))"
   by (rule fib_2)
 
-text {* \medskip Concrete Mathematics, page 280 *}
+text \<open>\medskip Concrete Mathematics, page 280\<close>
 
 lemma fib_add: "fib (Suc (n + k)) = fib (Suc k) * fib (Suc n) + fib k * fib n"
 proof (induct n rule: fib.induct)
@@ -60,10 +60,10 @@
   by (case_tac n, auto simp add: fib_Suc_gr_0) 
 
 
-text {*
+text \<open>
   \medskip Concrete Mathematics, page 278: Cassini's identity.  The proof is
   much easier using integers, not natural numbers!
-*}
+\<close>
 
 lemma fib_Cassini_int:
  "int (fib (Suc (Suc n)) * fib n) =
@@ -79,8 +79,8 @@
   with "3.hyps" show ?case by (simp add: fib.simps add_mult_distrib add_mult_distrib2)
 qed
 
-text{*We now obtain a version for the natural numbers via the coercion 
-   function @{term int}.*}
+text\<open>We now obtain a version for the natural numbers via the coercion 
+   function @{term int}.\<close>
 theorem fib_Cassini:
  "fib (Suc (Suc n)) * fib n =
   (if n mod 2 = 0 then fib (Suc n) * fib (Suc n) - 1
@@ -92,7 +92,7 @@
   done
 
 
-text {* \medskip Toward Law 6.111 of Concrete Mathematics *}
+text \<open>\medskip Toward Law 6.111 of Concrete Mathematics\<close>
 
 lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (Suc n)) = Suc 0"
   apply (induct n rule: fib.induct)
@@ -135,7 +135,7 @@
   qed
 qed
 
-lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"  -- {* Law 6.111 *}
+lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"  -- \<open>Law 6.111\<close>
   apply (induct m n rule: gcd_induct)
   apply (simp_all add: gcd_non_0 gcd_commute gcd_fib_mod)
   done
diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/Finite2.thy
--- a/src/HOL/Old_Number_Theory/Finite2.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Finite2.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -2,19 +2,19 @@
     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
 *)
 
-section {*Finite Sets and Finite Sums*}
+section \<open>Finite Sets and Finite Sums\<close>
 
 theory Finite2
 imports IntFact "~~/src/HOL/Library/Infinite_Set"
 begin
 
-text{*
+text\<open>
   These are useful for combinatorial and number-theoretic counting
   arguments.
-*}
+\<close>
 
 
-subsection {* Useful properties of sums and products *}
+subsection \<open>Useful properties of sums and products\<close>
 
 lemma setsum_same_function_zcong:
   assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
@@ -48,7 +48,7 @@
   by (induct set: finite) (auto simp add: distrib_left)
 
 
-subsection {* Cardinality of explicit finite sets *}
+subsection \<open>Cardinality of explicit finite sets\<close>
 
 lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B"
 by (simp add: finite_subset)
@@ -104,7 +104,7 @@
   also have "... = Suc (card {y. y < n})"
     by (rule card_insert_disjoint) (auto simp add: bdd_nat_set_l_finite)
   finally show "card {y. y < Suc n} = Suc n"
-    using `card {y. y < n} = n` by simp
+    using \<open>card {y. y < n} = n\<close> by simp
 qed
 
 lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x"
@@ -121,7 +121,7 @@
     by (auto simp add: inj_on_def)
   hence "card (int ` {y. y < nat n}) = card {y. y < nat n}"
     by (rule card_image)
-  also from `0 \<le> n` have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}"
+  also from \<open>0 \<le> n\<close> have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}"
     apply (auto simp add: zless_nat_eq_int_zless image_def)
     apply (rule_tac x = "nat x" in exI)
     apply (auto simp add: nat_0_le)
@@ -150,7 +150,7 @@
   hence "card ((%x. x+1) ` {x. 0 \<le> x & x < n}) =
      card {x. 0 \<le> x & x < n}"
     by (rule card_image)
-  also from `0 \<le> n` have "... = nat n"
+  also from \<open>0 \<le> n\<close> have "... = nat n"
     by (rule card_bdd_int_set_l)
   also have "(%x. x + 1) ` {x. 0 \<le> x & x < n} = {x. 0 < x & x<= n}"
     apply (auto simp add: image_def)
diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/Gauss.thy
--- a/src/HOL/Old_Number_Theory/Gauss.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Gauss.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -2,7 +2,7 @@
     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
 *)
 
-section {* Gauss' Lemma *}
+section \<open>Gauss' Lemma\<close>
 
 theory Gauss
 imports Euler
@@ -26,7 +26,7 @@
 definition "F = (%x. (p - x)) ` E"
 
 
-subsection {* Basic properties of p *}
+subsection \<open>Basic properties of p\<close>
 
 lemma p_odd: "p \<in> zOdd"
   by (auto simp add: p_prime p_g_2 zprime_zOdd_eq_grt_2)
@@ -64,7 +64,7 @@
   done
 
 
-subsection {* Basic Properties of the Gauss Sets *}
+subsection \<open>Basic Properties of the Gauss Sets\<close>
 
 lemma finite_A: "finite (A)"
 by (auto simp add: A_def)
@@ -272,7 +272,7 @@
 by(rule all_relprime_prod_relprime[OF finite_A all_A_relprime])
 
 
-subsection {* Relationships Between Gauss Sets *}
+subsection \<open>Relationships Between Gauss Sets\<close>
 
 lemma B_card_eq_A: "card B = card A"
   using finite_A by (simp add: finite_A B_def inj_on_xa_A card_image)
@@ -434,7 +434,7 @@
 qed
 
 
-subsection {* Gauss' Lemma *}
+subsection \<open>Gauss' Lemma\<close>
 
 lemma aux: "setprod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = setprod id A * a ^ card A"
   by (auto simp add: finite_E neg_one_special)
diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/Int2.thy
--- a/src/HOL/Old_Number_Theory/Int2.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Int2.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -2,7 +2,7 @@
     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
 *)
 
-section {*Integers: Divisibility and Congruences*}
+section \<open>Integers: Divisibility and Congruences\<close>
 
 theory Int2
 imports Finite2 WilsonRuss
@@ -12,7 +12,7 @@
   where "MultInv p x = x ^ nat (p - 2)"
 
 
-subsection {* Useful lemmas about dvd and powers *}
+subsection \<open>Useful lemmas about dvd and powers\<close>
 
 lemma zpower_zdvd_prop1:
   "0 < n \<Longrightarrow> p dvd y \<Longrightarrow> p dvd ((y::int) ^ n)"
@@ -47,12 +47,12 @@
   assumes "0 < z" and "(x::int) < y * z"
   shows "x div z < y"
 proof -
-  from `0 < z` have modth: "x mod z \<ge> 0" by simp
+  from \<open>0 < z\<close> have modth: "x mod z \<ge> 0" by simp
   have "(x div z) * z \<le> (x div z) * z" by simp
   then have "(x div z) * z \<le> (x div z) * z + x mod z" using modth by arith 
   also have "\<dots> = x"
     by (auto simp add: zmod_zdiv_equality [symmetric] ac_simps)
-  also note `x < y * z`
+  also note \<open>x < y * z\<close>
   finally show ?thesis
     apply (auto simp add: mult_less_cancel_right)
     using assms apply arith
@@ -66,7 +66,7 @@
   from assms have "x < (y + 1) * z" by (auto simp add: int_distrib)
   then have "x div z < y + 1"
     apply (rule_tac y = "y + 1" in div_prop1)
-    apply (auto simp add: `0 < z`)
+    apply (auto simp add: \<open>0 < z\<close>)
     done
   then show ?thesis by auto
 qed
@@ -79,7 +79,7 @@
 qed
 
 
-subsection {* Useful properties of congruences *}
+subsection \<open>Useful properties of congruences\<close>
 
 lemma zcong_eq_zdvd_prop: "[x = 0](mod p) = (p dvd x)"
   by (auto simp add: zcong_def)
@@ -142,7 +142,7 @@
     by auto
   then have "p dvd 2"
     by (auto simp add: dvd_def zcong_def)
-  with `2 < p` show False
+  with \<open>2 < p\<close> show False
     by (auto simp add: zdvd_not_zless)
 qed
 
@@ -174,7 +174,7 @@
   by (induct set: finite) (auto simp add: zgcd_zgcd_zmult)
 
 
-subsection {* Some properties of MultInv *}
+subsection \<open>Some properties of MultInv\<close>
 
 lemma MultInv_prop1: "[| 2 < p; [x = y] (mod p) |] ==>
     [(MultInv p x) = (MultInv p y)] (mod p)"
diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/IntFact.thy
--- a/src/HOL/Old_Number_Theory/IntFact.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/IntFact.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -3,19 +3,19 @@
     Copyright   2000  University of Cambridge
 *)
 
-section {* Factorial on integers *}
+section \<open>Factorial on integers\<close>
 
 theory IntFact
 imports IntPrimes
 begin
 
-text {*
+text \<open>
   Factorial on integers and recursively defined set including all
   Integers from @{text 2} up to @{text a}.  Plus definition of product
   of finite set.
 
   \bigskip
-*}
+\<close>
 
 fun zfact :: "int => int"
   where "zfact n = (if n \<le> 0 then 1 else n * zfact (n - 1))"
@@ -24,10 +24,10 @@
   where "d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})"
 
 
-text {*
+text \<open>
   \medskip @{term d22set} --- recursively defined set including all
   integers from @{text 2} up to @{text a}
-*}
+\<close>
 
 declare d22set.simps [simp del]
 
diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/IntPrimes.thy
--- a/src/HOL/Old_Number_Theory/IntPrimes.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -3,22 +3,22 @@
     Copyright   2000  University of Cambridge
 *)
 
-section {* Divisibility and prime numbers (on integers) *}
+section \<open>Divisibility and prime numbers (on integers)\<close>
 
 theory IntPrimes
 imports Primes
 begin
 
-text {*
+text \<open>
   The @{text dvd} relation, GCD, Euclid's extended algorithm, primes,
   congruences (all on the Integers).  Comparable to theory @{text
   Primes}, but @{text dvd} is included here as it is not present in
   main HOL.  Also includes extended GCD and congruences not present in
   @{text Primes}.
-*}
+\<close>
 
 
-subsection {* Definitions *}
+subsection \<open>Definitions\<close>
 
 fun xzgcda :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int => (int * int * int)"
 where
@@ -38,7 +38,7 @@
   where "[a = b] (mod m) = (m dvd (a - b))"
 
 
-subsection {* Euclid's Algorithm and GCD *}
+subsection \<open>Euclid's Algorithm and GCD\<close>
 
 
 lemma zrelprime_zdvd_zmult_aux:
@@ -55,8 +55,8 @@
 lemma zgcd_geq_zero: "0 <= zgcd x y"
   by (auto simp add: zgcd_def)
 
-text{*This is merely a sanity check on zprime, since the previous version
-      denoted the empty set.*}
+text\<open>This is merely a sanity check on zprime, since the previous version
+      denoted the empty set.\<close>
 lemma "zprime 2"
   apply (auto simp add: zprime_def) 
   apply (frule zdvd_imp_le, simp) 
@@ -109,7 +109,7 @@
 
 
 
-subsection {* Congruences *}
+subsection \<open>Congruences\<close>
 
 lemma zcong_1 [simp]: "[a = b] (mod 1)"
   by (unfold zcong_def, auto)
@@ -281,7 +281,7 @@
   apply (simp add: linorder_neq_iff)
   apply (erule disjE)  
    prefer 2 apply (simp add: zcong_zmod_eq)
-  txt{*Remainding case: @{term "m<0"}*}
+  txt\<open>Remainding case: @{term "m<0"}\<close>
   apply (rule_tac t = m in minus_minus [THEN subst])
   apply (subst zcong_zminus)
   apply (subst zcong_zmod_eq, arith)
@@ -289,14 +289,14 @@
   apply (simp add: zmod_zminus2_eq_if del: neg_mod_bound)
   done
 
-subsection {* Modulo *}
+subsection \<open>Modulo\<close>
 
 lemma zmod_zdvd_zmod:
     "0 < (m::int) ==> m dvd b ==> (a mod b mod m) = (a mod m)"
   by (rule mod_mod_cancel) 
 
 
-subsection {* Extended GCD *}
+subsection \<open>Extended GCD\<close>
 
 declare xzgcda.simps [simp del]
 
@@ -336,7 +336,7 @@
   done
 
 
-text {* \medskip @{term xzgcd} linear *}
+text \<open>\medskip @{term xzgcd} linear\<close>
 
 lemma xzgcda_linear_aux1:
   "(a - r * b) * m + (c - r * d) * (n::int) =
@@ -399,7 +399,7 @@
     zgcd a n = 1 ==> \<exists>!x. 0 \<le> x \<and> x < n \<and> [a * x = b] (mod n)"
   apply auto
    apply (rule_tac [2] zcong_zless_imp_eq)
-       apply (tactic {* stac @{context} (@{thm zcong_cancel2} RS sym) 6 *})
+       apply (tactic \<open>stac @{context} (@{thm zcong_cancel2} RS sym) 6\<close>)
          apply (rule_tac [8] zcong_trans)
           apply (simp_all (no_asm_simp))
    prefer 2
diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/Legacy_GCD.thy
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -3,40 +3,40 @@
     Copyright   1996  University of Cambridge
 *)
 
-section {* The Greatest Common Divisor *}
+section \<open>The Greatest Common Divisor\<close>
 
 theory Legacy_GCD
 imports Main
 begin
 
-text {*
+text \<open>
   See @{cite davenport92}. \bigskip
-*}
+\<close>
 
-subsection {* Specification of GCD on nats *}
+subsection \<open>Specification of GCD on nats\<close>
 
 definition
-  is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- {* @{term gcd} as a relation *}
+  is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- \<open>@{term gcd} as a relation\<close>
   "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
     (\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
 
-text {* Uniqueness *}
+text \<open>Uniqueness\<close>
 
 lemma is_gcd_unique: "is_gcd a b m \<Longrightarrow> is_gcd a b n \<Longrightarrow> m = n"
   by (simp add: is_gcd_def) (blast intro: dvd_antisym)
 
-text {* Connection to divides relation *}
+text \<open>Connection to divides relation\<close>
 
 lemma is_gcd_dvd: "is_gcd a b m \<Longrightarrow> k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd m"
   by (auto simp add: is_gcd_def)
 
-text {* Commutativity *}
+text \<open>Commutativity\<close>
 
 lemma is_gcd_commute: "is_gcd m n k = is_gcd n m k"
   by (auto simp add: is_gcd_def)
 
 
-subsection {* GCD on nat by Euclid's algorithm *}
+subsection \<open>GCD on nat by Euclid's algorithm\<close>
 
 fun gcd :: "nat => nat => nat"
   where "gcd m n = (if n = 0 then m else gcd n (m mod n))"
@@ -68,10 +68,10 @@
 
 declare gcd.simps [simp del]
 
-text {*
+text \<open>
   \medskip @{term "gcd m n"} divides @{text m} and @{text n}.  The
   conjunctions don't seem provable separately.
-*}
+\<close>
 
 lemma gcd_dvd1 [iff, algebra]: "gcd m n dvd m"
   and gcd_dvd2 [iff, algebra]: "gcd m n dvd n"
@@ -80,24 +80,24 @@
   apply (blast dest: dvd_mod_imp_dvd)
   done
 
-text {*
+text \<open>
   \medskip Maximality: for all @{term m}, @{term n}, @{term k}
   naturals, if @{term k} divides @{term m} and @{term k} divides
   @{term n} then @{term k} divides @{term "gcd m n"}.
-*}
+\<close>
 
 lemma gcd_greatest: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
   by (induct m n rule: gcd_induct) (simp_all add: gcd_non_0 dvd_mod)
 
-text {*
+text \<open>
   \medskip Function gcd yields the Greatest Common Divisor.
-*}
+\<close>
 
 lemma is_gcd: "is_gcd m n (gcd m n) "
   by (simp add: is_gcd_def gcd_greatest)
 
 
-subsection {* Derived laws for GCD *}
+subsection \<open>Derived laws for GCD\<close>
 
 lemma gcd_greatest_iff [iff, algebra]: "k dvd gcd m n \<longleftrightarrow> k dvd m \<and> k dvd n"
   by (blast intro!: gcd_greatest intro: dvd_trans)
@@ -125,12 +125,12 @@
 lemma nat_gcd_1_left [simp, algebra]: "gcd 1 m = 1"
   unfolding One_nat_def by (rule gcd_1_left)
 
-text {*
+text \<open>
   \medskip Multiplication laws
-*}
+\<close>
 
 lemma gcd_mult_distrib2: "k * gcd m n = gcd (k * m) (k * n)"
-    -- {* @{cite \<open>page 27\<close> davenport92} *}
+    -- \<open>@{cite \<open>page 27\<close> davenport92}\<close>
   apply (induct m n rule: gcd_induct)
    apply simp
   apply (case_tac "k = 0")
@@ -165,7 +165,7 @@
   done
 
 
-text {* \medskip Addition laws *}
+text \<open>\medskip Addition laws\<close>
 
 lemma gcd_add1 [simp, algebra]: "gcd (m + n) n = gcd m n"
   by (cases "n = 0") (auto simp add: gcd_non_0)
@@ -190,9 +190,9 @@
 lemma gcd_dvd_prod: "gcd m n dvd m * n" 
   using mult_dvd_mono [of 1] by auto
 
-text {*
+text \<open>
   \medskip Division by gcd yields rrelatively primes.
-*}
+\<close>
 
 lemma div_gcd_relprime:
   assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
@@ -313,7 +313,7 @@
 done
 
 
-text {* We can get a stronger version with a nonzeroness assumption. *}
+text \<open>We can get a stronger version with a nonzeroness assumption.\<close>
 lemma divides_le: "m dvd n ==> m <= n \<or> n = (0::nat)" by (auto simp add: dvd_def)
 
 lemma bezout_add_strong: assumes nz: "a \<noteq> (0::nat)"
@@ -449,7 +449,7 @@
 qed
 
 
-subsection {* LCM defined by GCD *}
+subsection \<open>LCM defined by GCD\<close>
 
 
 definition
@@ -562,7 +562,7 @@
   done
 
 
-subsection {* GCD and LCM on integers *}
+subsection \<open>GCD and LCM on integers\<close>
 
 definition
   zgcd :: "int \<Rightarrow> int \<Rightarrow> int" where
@@ -595,7 +595,7 @@
 proof -
   assume "int (gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>)) = 1" "i dvd k * j"
   then have g: "gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>) = 1" by simp
-  from `i dvd k * j` obtain h where h: "k*j = i*h" unfolding dvd_def by blast
+  from \<open>i dvd k * j\<close> obtain h where h: "k*j = i*h" unfolding dvd_def by blast
   have th: "nat \<bar>i\<bar> dvd nat \<bar>k\<bar> * nat \<bar>j\<bar>"
     unfolding dvd_def
     by (rule_tac x= "nat \<bar>h\<bar>" in exI, simp add: h nat_abs_mult_distrib [symmetric])
@@ -620,7 +620,7 @@
   let ?k' = "nat \<bar>k\<bar>"
   let ?m' = "nat \<bar>m\<bar>"
   let ?n' = "nat \<bar>n\<bar>"
-  from `k dvd m` and `k dvd n` have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
+  from \<open>k dvd m\<close> and \<open>k dvd n\<close> have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
     unfolding zdvd_int by (simp_all only: int_nat_abs abs_dvd_iff dvd_abs_iff)
   from gcd_greatest [OF dvd'] have "int (nat \<bar>k\<bar>) dvd zgcd m n"
     unfolding zgcd_def by (simp only: zdvd_int)
@@ -696,7 +696,7 @@
   done
 
 lemmas zgcd_ac = zgcd_assoc zgcd_commute zgcd_left_commute
-  -- {* addition is an AC-operator *}
+  -- \<open>addition is an AC-operator\<close>
 
 lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd m n = zgcd (k * m) (k * n)"
   by (simp del: minus_mult_right [symmetric]
@@ -728,7 +728,7 @@
 lemma dvd_imp_dvd_zlcm1:
   assumes "k dvd i" shows "k dvd (zlcm i j)"
 proof -
-  have "nat(abs k) dvd nat(abs i)" using `k dvd i`
+  have "nat(abs k) dvd nat(abs i)" using \<open>k dvd i\<close>
     by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
   thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
 qed
@@ -736,7 +736,7 @@
 lemma dvd_imp_dvd_zlcm2:
   assumes "k dvd j" shows "k dvd (zlcm i j)"
 proof -
-  have "nat(abs k) dvd nat(abs j)" using `k dvd j`
+  have "nat(abs k) dvd nat(abs j)" using \<open>k dvd j\<close>
     by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
   thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
 qed
diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/Pocklington.thy
--- a/src/HOL/Old_Number_Theory/Pocklington.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Amine Chaieb
 *)
 
-section {* Pocklington's Theorem for Primes *}
+section \<open>Pocklington's Theorem for Primes\<close>
 
 theory Pocklington
 imports Primes
diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/Primes.thy
--- a/src/HOL/Old_Number_Theory/Primes.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Primes.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   1996  University of Cambridge
 *)
 
-section {* Primality on nat *}
+section \<open>Primality on nat\<close>
 
 theory Primes
 imports Complex_Main Legacy_GCD
@@ -27,11 +27,11 @@
   apply (metis gcd_dvd1 gcd_dvd2)
   done
 
-text {*
+text \<open>
   This theorem leads immediately to a proof of the uniqueness of
   factorization.  If @{term p} divides a product of primes then it is
   one of those primes.
-*}
+\<close>
 
 lemma prime_dvd_mult: "prime p ==> p dvd m * n ==> p dvd m \<or> p dvd n"
   by (blast intro: relprime_dvd_mult prime_imp_relprime)
@@ -92,7 +92,7 @@
   ultimately show ?thesis by blast  
 qed
 
-text {* Elementary theory of divisibility *}
+text \<open>Elementary theory of divisibility\<close>
 lemma divides_ge: "(a::nat) dvd b \<Longrightarrow> b = 0 \<or> a \<le> b" unfolding dvd_def by auto
 lemma divides_antisym: "(x::nat) dvd y \<and> y dvd x \<longleftrightarrow> x = y"
   using dvd_antisym[of x y] by auto
@@ -176,7 +176,7 @@
 lemma divides_rexp: 
   "x dvd y \<Longrightarrow> (x::nat) dvd (y^(Suc n))" by (simp add: dvd_mult2[of x y])
 
-text {* Coprimality *}
+text \<open>Coprimality\<close>
 
 lemma coprime: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
 using gcd_unique[of 1 a b, simplified] by (auto simp add: coprime_def)
@@ -379,7 +379,7 @@
 qed
 
 
-text {* A binary form of the Chinese Remainder Theorem. *}
+text \<open>A binary form of the Chinese Remainder Theorem.\<close>
 
 lemma chinese_remainder: assumes ab: "coprime a b" and a:"a \<noteq> 0" and b:"b \<noteq> 0"
   shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b"
@@ -397,9 +397,9 @@
   thus ?thesis by blast
 qed
 
-text {* Primality *}
+text \<open>Primality\<close>
 
-text {* A few useful theorems about primes *}
+text \<open>A few useful theorems about primes\<close>
 
 lemma prime_0[simp]: "~prime 0" by (simp add: prime_def)
 lemma prime_1[simp]: "~ prime 1"  by (simp add: prime_def)
@@ -591,7 +591,7 @@
 lemma prime_odd: "prime p \<Longrightarrow> p = 2 \<or> odd p" unfolding prime_def by auto
 
 
-text {* One property of coprimality is easier to prove via prime factors. *}
+text \<open>One property of coprimality is easier to prove via prime factors.\<close>
 
 lemma prime_divprod_pow: 
   assumes p: "prime p" and ab: "coprime a b" and pab: "p^n dvd a * b"
@@ -714,7 +714,7 @@
 ultimately show ?ths by blast
 qed
 
-text {* More useful lemmas. *}
+text \<open>More useful lemmas.\<close>
 lemma prime_product: 
   assumes "prime (p * q)"
   shows "p = 1 \<or> q = 1"
@@ -722,7 +722,7 @@
   from assms have 
     "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
     unfolding prime_def by auto
-  from `1 < p * q` have "p \<noteq> 0" by (cases p) auto
+  from \<open>1 < p * q\<close> have "p \<noteq> 0" by (cases p) auto
   then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
   have "p dvd p * q" by simp
   then have "p = 1 \<or> p = p * q" by (rule P)
diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
--- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -2,16 +2,16 @@
     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
 *)
 
-section {* The law of Quadratic reciprocity *}
+section \<open>The law of Quadratic reciprocity\<close>
 
 theory Quadratic_Reciprocity
 imports Gauss
 begin
 
-text {*
+text \<open>
   Lemmas leading up to the proof of theorem 3.3 in Niven and
   Zuckerman's presentation.
-*}
+\<close>
 
 context GAUSS
 begin
@@ -153,7 +153,7 @@
   done
 
 
-subsection {* Stuff about S, S1 and S2 *}
+subsection \<open>Stuff about S, S1 and S2\<close>
 
 locale QRTEMP =
   fixes p     :: "int"
diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/Residues.thy
--- a/src/HOL/Old_Number_Theory/Residues.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Residues.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -2,15 +2,15 @@
     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
 *)
 
-section {* Residue Sets *}
+section \<open>Residue Sets\<close>
 
 theory Residues
 imports Int2
 begin
 
-text {*
+text \<open>
   \medskip Define the residue of a set, the standard residue,
-  quadratic residues, and prove some basic properties. *}
+  quadratic residues, and prove some basic properties.\<close>
 
 definition ResSet :: "int => int set => bool"
   where "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))"
@@ -33,7 +33,7 @@
   where "SRStar p = {x. (0 < x) & (x < p)}"
 
 
-subsection {* Some useful properties of StandardRes *}
+subsection \<open>Some useful properties of StandardRes\<close>
 
 lemma StandardRes_prop1: "[x = StandardRes m x] (mod m)"
   by (auto simp add: StandardRes_def zcong_zmod)
@@ -61,7 +61,7 @@
   by (auto simp add: StandardRes_def zcong_eq_zdvd_prop dvd_def) 
 
 
-subsection {* Relations between StandardRes, SRStar, and SR *}
+subsection \<open>Relations between StandardRes, SRStar, and SR\<close>
 
 lemma SRStar_SR_prop: "x \<in> SRStar p ==> x \<in> SR p"
   by (auto simp add: SRStar_def SR_def)
@@ -115,7 +115,7 @@
   by (auto simp add: SRStar_def bdd_int_set_l_l_finite)
 
 
-subsection {* Properties relating ResSets with StandardRes *}
+subsection \<open>Properties relating ResSets with StandardRes\<close>
 
 lemma aux: "x mod m = y mod m ==> [x = y] (mod m)"
   apply (subgoal_tac "x = y ==> [x = y](mod m)")
@@ -158,7 +158,7 @@
   by (auto simp add: ResSet_def)
 
 
-subsection {* Property for SRStar *}
+subsection \<open>Property for SRStar\<close>
 
 lemma ResSet_SRStar_prop: "ResSet p (SRStar p)"
   by (auto simp add: SRStar_def ResSet_def zcong_zless_imp_eq)
diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/WilsonBij.thy
--- a/src/HOL/Old_Number_Theory/WilsonBij.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonBij.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -3,20 +3,20 @@
     Copyright   2000  University of Cambridge
 *)
 
-section {* Wilson's Theorem using a more abstract approach *}
+section \<open>Wilson's Theorem using a more abstract approach\<close>
 
 theory WilsonBij
 imports BijectionRel IntFact
 begin
 
-text {*
+text \<open>
   Wilson's Theorem using a more ``abstract'' approach based on
   bijections between sets.  Does not use Fermat's Little Theorem
   (unlike Russinoff).
-*}
+\<close>
 
 
-subsection {* Definitions and lemmas *}
+subsection \<open>Definitions and lemmas\<close>
 
 definition reciR :: "int => int => int => bool"
   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)"
@@ -28,7 +28,7 @@
      else 0)"
 
 
-text {* \medskip Inverse *}
+text \<open>\medskip Inverse\<close>
 
 lemma inv_correct:
   "zprime p ==> 0 < a ==> a < p
@@ -47,7 +47,7 @@
 
 lemma inv_not_0:
   "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> 0"
-  -- {* same as @{text WilsonRuss} *}
+  -- \<open>same as @{text WilsonRuss}\<close>
   apply safe
   apply (cut_tac a = a and p = p in inv_is_inv)
      apply (unfold zcong_def)
@@ -56,7 +56,7 @@
 
 lemma inv_not_1:
   "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> 1"
-  -- {* same as @{text WilsonRuss} *}
+  -- \<open>same as @{text WilsonRuss}\<close>
   apply safe
   apply (cut_tac a = a and p = p in inv_is_inv)
      prefer 4
@@ -67,7 +67,7 @@
   done
 
 lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
-  -- {* same as @{text WilsonRuss} *}
+  -- \<open>same as @{text WilsonRuss}\<close>
   apply (unfold zcong_def)
   apply (simp add: diff_diff_eq diff_diff_eq2 right_diff_distrib)
   apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
@@ -81,7 +81,7 @@
 
 lemma inv_not_p_minus_1:
   "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> p - 1"
-  -- {* same as @{text WilsonRuss} *}
+  -- \<open>same as @{text WilsonRuss}\<close>
   apply safe
   apply (cut_tac a = a and p = p in inv_is_inv)
      apply auto
@@ -91,10 +91,10 @@
        apply auto
   done
 
-text {*
+text \<open>
   Below is slightly different as we don't expand @{term [source] inv}
   but use ``@{text correct}'' theorems.
-*}
+\<close>
 
 lemma inv_g_1: "zprime p ==> 1 < a ==> a < p - 1 ==> 1 < inv p a"
   apply (subgoal_tac "inv p a \<noteq> 1")
@@ -111,13 +111,13 @@
 
 lemma inv_less_p_minus_1:
   "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a < p - 1"
-  -- {* ditto *}
+  -- \<open>ditto\<close>
   apply (subst order_less_le)
   apply (simp add: inv_not_p_minus_1 inv_less)
   done
 
 
-text {* \medskip Bijection *}
+text \<open>\medskip Bijection\<close>
 
 lemma aux1: "1 < x ==> 0 \<le> (x::int)"
   apply auto
@@ -139,9 +139,9 @@
   apply (unfold inj_on_def)
   apply auto
   apply (rule zcong_zless_imp_eq)
-      apply (tactic {* stac @{context} (@{thm zcong_cancel} RS sym) 5 *})
+      apply (tactic \<open>stac @{context} (@{thm zcong_cancel} RS sym) 5\<close>)
         apply (rule_tac [7] zcong_trans)
-         apply (tactic {* stac @{context} @{thm zcong_sym} 8 *})
+         apply (tactic \<open>stac @{context} @{thm zcong_sym} 8\<close>)
          apply (erule_tac [7] inv_is_inv)
           apply (tactic "asm_simp_tac @{context} 9")
           apply (erule_tac [9] inv_is_inv)
@@ -192,15 +192,15 @@
   apply (unfold reciR_def uniqP_def)
   apply auto
    apply (rule zcong_zless_imp_eq)
-       apply (tactic {* stac @{context} (@{thm zcong_cancel2} RS sym) 5 *})
+       apply (tactic \<open>stac @{context} (@{thm zcong_cancel2} RS sym) 5\<close>)
          apply (rule_tac [7] zcong_trans)
-          apply (tactic {* stac @{context} @{thm zcong_sym} 8 *})
+          apply (tactic \<open>stac @{context} @{thm zcong_sym} 8\<close>)
           apply (rule_tac [6] zless_zprime_imp_zrelprime)
             apply auto
   apply (rule zcong_zless_imp_eq)
-      apply (tactic {* stac @{context} (@{thm zcong_cancel} RS sym) 5 *})
+      apply (tactic \<open>stac @{context} (@{thm zcong_cancel} RS sym) 5\<close>)
         apply (rule_tac [7] zcong_trans)
-         apply (tactic {* stac @{context} @{thm zcong_sym} 8 *})
+         apply (tactic \<open>stac @{context} @{thm zcong_sym} 8\<close>)
          apply (rule_tac [6] zless_zprime_imp_zrelprime)
            apply auto
   done
@@ -220,7 +220,7 @@
   done
 
 
-subsection {* Wilson *}
+subsection \<open>Wilson\<close>
 
 lemma bijER_zcong_prod_1:
     "zprime p ==> A \<in> bijER (reciR p) ==> [\<Prod>A = 1] (mod p)"
diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/WilsonRuss.thy
--- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -3,18 +3,18 @@
     Copyright   2000  University of Cambridge
 *)
 
-section {* Wilson's Theorem according to Russinoff *}
+section \<open>Wilson's Theorem according to Russinoff\<close>
 
 theory WilsonRuss
 imports EulerFermat
 begin
 
-text {*
+text \<open>
   Wilson's Theorem following quite closely Russinoff's approach
   using Boyer-Moore (using finite sets instead of lists, though).
-*}
+\<close>
 
-subsection {* Definitions and lemmas *}
+subsection \<open>Definitions and lemmas\<close>
 
 definition inv :: "int => int => int"
   where "inv p a = (a^(nat (p - 2))) mod p"
@@ -26,7 +26,7 @@
       in (if a \<in> ws then ws else insert a (insert (inv p a) ws)) else {})"
 
 
-text {* \medskip @{term [source] inv} *}
+text \<open>\medskip @{term [source] inv}\<close>
 
 lemma inv_is_inv_aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)"
   by (subst int_int_eq [symmetric]) auto
@@ -149,7 +149,7 @@
   done
 
 
-text {* \medskip @{term wset} *}
+text \<open>\medskip @{term wset}\<close>
 
 declare wset.simps [simp del]
 
@@ -252,7 +252,7 @@
    apply (subst wset.simps)
    apply (auto, unfold Let_def, auto)
   apply (subst setprod.insert)
-    apply (tactic {* stac @{context} @{thm setprod.insert} 3 *})
+    apply (tactic \<open>stac @{context} @{thm setprod.insert} 3\<close>)
       apply (subgoal_tac [5]
         "zcong (a * inv p a * (\<Prod>x\<in>wset (a - 1) p. x)) (1 * 1) p")
        prefer 5
@@ -281,7 +281,7 @@
   done
 
 
-subsection {* Wilson *}
+subsection \<open>Wilson\<close>
 
 lemma prime_g_5: "zprime p \<Longrightarrow> p \<noteq> 2 \<Longrightarrow> p \<noteq> 3 ==> 5 \<le> p"
   apply (unfold zprime_def dvd_def)