# HG changeset patch
# User wenzelm
# Date 1541712549 -3600
# Node ID 15e9ed5b28fbf4974c6e1dd2b52dae09e52ac22d
# Parent  4cb70e7e36b9a34b159689a634e025358c278d43
isabelle update_cartouches -t;

diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/Benchmarks/ROOT
--- a/src/Benchmarks/ROOT	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/Benchmarks/ROOT	Thu Nov 08 22:29:09 2018 +0100
@@ -1,9 +1,9 @@
 chapter HOL
 
 session "HOL-Datatype_Benchmark" in Datatype_Benchmark = "HOL-Library" +
-  description {*
+  description \<open>
     Big (co)datatypes.
-  *}
+\<close>
   theories
     Brackin
     IsaFoR
@@ -17,8 +17,8 @@
     Needham_Schroeder_Unguided_Attacker_Example
 
 session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
-  description {*
+  description \<open>
     Big records.
-  *}
+\<close>
   theories
     Record_Benchmark
diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/CCL/ROOT
--- a/src/CCL/ROOT	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/CCL/ROOT	Thu Nov 08 22:29:09 2018 +0100
@@ -1,7 +1,7 @@
 chapter CCL
 
 session CCL = Pure +
-  description {*
+  description \<open>
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
@@ -9,7 +9,7 @@
 
     A computational logic for an untyped functional language with
     evaluation to weak head-normal form.
-  *}
+\<close>
   sessions
     FOL
   theories
diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/CTT/ROOT
--- a/src/CTT/ROOT	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/CTT/ROOT	Thu Nov 08 22:29:09 2018 +0100
@@ -1,7 +1,7 @@
 chapter CTT
 
 session CTT = Pure +
-  description {*
+  description \<open>
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
@@ -15,7 +15,7 @@
 
     Simon Thompson, Type Theory and Functional Programming (Addison-Wesley,
     1991)
-  *}
+\<close>
   options [thy_output_source]
   theories
     CTT
diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/Cube/ROOT
--- a/src/Cube/ROOT	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/Cube/ROOT	Thu Nov 08 22:29:09 2018 +0100
@@ -1,7 +1,7 @@
 chapter Cube
 
 session Cube = Pure +
-  description {*
+  description \<open>
     Author:     Tobias Nipkow
     Copyright   1992  University of Cambridge
 
@@ -12,5 +12,5 @@
 
     For more information about the Lambda-Cube, see H. Barendregt, Introduction
     to Generalised Type Systems, J. Functional Programming.
-  *}
+\<close>
   theories Example
diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/FOL/ROOT
--- a/src/FOL/ROOT	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/FOL/ROOT	Thu Nov 08 22:29:09 2018 +0100
@@ -1,7 +1,7 @@
 chapter FOL
 
 session FOL = Pure +
-  description {*
+  description \<open>
     First-Order Logic with Natural Deduction (constructive and classical
     versions). For a classical sequent calculus, see Isabelle/LK.
 
@@ -14,16 +14,16 @@
     Antony Galton, Logic for Information Technology (Wiley, 1990)
 
     Michael Dummett, Elements of Intuitionism (Oxford, 1977)
-  *}
+\<close>
   theories
     IFOL (global)
     FOL (global)
   document_files "root.tex"
 
 session "FOL-ex" in ex = FOL +
-  description {*
+  description \<open>
     Examples for First-Order Logic.
-  *}
+\<close>
   theories
     Natural_Numbers
     Intro
diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/FOLP/ROOT
--- a/src/FOLP/ROOT	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/FOLP/ROOT	Thu Nov 08 22:29:09 2018 +0100
@@ -1,25 +1,25 @@
 chapter FOLP
 
 session FOLP = Pure +
-  description {*
+  description \<open>
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
     Modifed version of FOL that contains proof terms.
 
     Presence of unknown proof term means that matching does not behave as expected.
-  *}
+\<close>
   theories
     IFOLP (global)
     FOLP (global)
 
 session "FOLP-ex" in ex = FOLP +
-  description {*
+  description \<open>
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
     Examples for First-Order Logic.
-  *}
+\<close>
   theories
     Intro
     Nat
diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/HOL/Algebra/Group.thy	Thu Nov 08 22:29:09 2018 +0100
@@ -1394,7 +1394,7 @@
   then show "\<exists>I. greatest ?L I (Lower ?L A)" ..
 qed
 
-subsection\<open>Jeremy Avigad's @{text"More_Group"} material\<close>
+subsection\<open>Jeremy Avigad's \<open>More_Group\<close> material\<close>
 
 text \<open>
   Show that the units in any monoid give rise to a group.
diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/HOL/Algebra/Ring.thy	Thu Nov 08 22:29:09 2018 +0100
@@ -807,7 +807,7 @@
   "\<lbrakk> f \<in> ring_hom R S; g \<in> ring_hom S T \<rbrakk> \<Longrightarrow> g \<circ> f \<in> ring_hom R T"
   by (rule ring_hom_memI) (auto simp add: ring_hom_closed ring_hom_mult ring_hom_add ring_hom_one)
 
-subsection\<open>Jeremy Avigad's @{text"More_Finite_Product"} material\<close>
+subsection\<open>Jeremy Avigad's \<open>More_Finite_Product\<close> material\<close>
 
 (* need better simplification rules for rings *)
 (* the next one holds more generally for abelian groups *)
@@ -857,7 +857,7 @@
   "finite (Units R) \<Longrightarrow> a \<in> Units R \<Longrightarrow> a [^] card(Units R) = \<one>"
   by (metis comm_group.power_order_eq_one units_comm_group units_of_carrier units_of_one units_of_pow)
 
-subsection\<open>Jeremy Avigad's @{text"More_Ring"} material\<close>
+subsection\<open>Jeremy Avigad's \<open>More_Ring\<close> material\<close>
 
 lemma (in cring) field_intro2: 
   assumes "\<zero>\<^bsub>R\<^esub> \<noteq> \<one>\<^bsub>R\<^esub>" and un: "\<And>x. x \<in> carrier R - {\<zero>\<^bsub>R\<^esub>} \<Longrightarrow> x \<in> Units R"
diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/HOL/Algebra/Sylow.thy
--- a/src/HOL/Algebra/Sylow.thy	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/HOL/Algebra/Sylow.thy	Thu Nov 08 22:29:09 2018 +0100
@@ -8,7 +8,7 @@
 
 text \<open>See also @{cite "Kammueller-Paulson:1999"}.\<close>
 
-text \<open>The combinatorial argument is in theory @{text "Exponent"}.\<close>
+text \<open>The combinatorial argument is in theory \<open>Exponent\<close>.\<close>
 
 lemma le_extend_mult: "\<lbrakk>0 < c; a \<le> b\<rbrakk> \<Longrightarrow> a \<le> b * c"
   for c :: nat
diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Nov 08 22:29:09 2018 +0100
@@ -229,7 +229,7 @@
 proof -
   obtain A' where "A ** A' = mat 1" and "A' ** A = mat 1"
     using assms unfolding invertible_def by auto
-  with `k \<noteq> 0`
+  with \<open>k \<noteq> 0\<close>
   have "(k *\<^sub>R A) ** ((1/k) *\<^sub>R A') = mat 1" "((1/k) *\<^sub>R A') ** (k *\<^sub>R A) = mat 1"
     by (simp_all add: assms matrix_scalar_ac)
   thus "invertible (k *\<^sub>R A)"
diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/HOL/Analysis/Change_Of_Vars.thy
--- a/src/HOL/Analysis/Change_Of_Vars.thy	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Thu Nov 08 22:29:09 2018 +0100
@@ -625,7 +625,7 @@
     by (simp add: measure_linear_image \<open>linear f\<close> S f)
 qed
 
-subsection%important\<open>@{text F_sigma} and @{text G_delta} sets.\<close>(*FIX ME mv *)
+subsection%important\<open>\<open>F_sigma\<close> and \<open>G_delta\<close> sets.\<close>(*FIX ME mv *)
 
 (*https://en.wikipedia.org/wiki/F\<sigma>_set*)
 inductive%important fsigma :: "'a::topological_space set \<Rightarrow> bool" where
@@ -689,7 +689,7 @@
 lemma%unimportant gdelta_complement: "gdelta(- S) \<longleftrightarrow> fsigma S"
   using fsigma_imp_gdelta gdelta_imp_fsigma by force
 
-text\<open>A Lebesgue set is almost an @{text F_sigma} or @{text G_delta}.\<close>
+text\<open>A Lebesgue set is almost an \<open>F_sigma\<close> or \<open>G_delta\<close>.\<close>
 lemma%unimportant lebesgue_set_almost_fsigma:
   assumes "S \<in> sets lebesgue"
   obtains C T where "fsigma C" "negligible T" "C \<union> T = S" "disjnt C T"
diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Nov 08 22:29:09 2018 +0100
@@ -1228,7 +1228,7 @@
 proof%unimportant -
   obtain A' where "A ** A' = mat 1" and "A' ** A = mat 1"
     using assms unfolding invertible_def by auto
-  with `k \<noteq> 0`
+  with \<open>k \<noteq> 0\<close>
   have "(k *\<^sub>R A) ** ((1/k) *\<^sub>R A') = mat 1" "((1/k) *\<^sub>R A') ** (k *\<^sub>R A) = mat 1"
     by (simp_all add: assms matrix_scalar_ac)
   thus "invertible (k *\<^sub>R A)"
diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Thu Nov 08 22:29:09 2018 +0100
@@ -7957,7 +7957,7 @@
 qed
 
 
-subsection{*Orthogonal complement*}
+subsection\<open>Orthogonal complement\<close>
 
 definition orthogonal_comp ("_\<^sup>\<bottom>" [80] 80)
   where "orthogonal_comp W \<equiv> {x. \<forall>y \<in> W. orthogonal y x}"
diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/HOL/Eisbach/Eisbach.thy
--- a/src/HOL/Eisbach/Eisbach.thy	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/HOL/Eisbach/Eisbach.thy	Thu Nov 08 22:29:09 2018 +0100
@@ -90,9 +90,9 @@
 \<close>
 
 
-text \<open>The following @{text fails} and @{text succeeds} methods protect the goal from the effect
+text \<open>The following \<open>fails\<close> and \<open>succeeds\<close> methods protect the goal from the effect
       of a method, instead simply determining whether or not it can be applied to the current goal.
-      The @{text fails} method inverts success, only succeeding if the given method would fail.\<close>
+      The \<open>fails\<close> method inverts success, only succeeding if the given method would fail.\<close>
 
 method_setup fails =
  \<open>Method.text_closure >> (fn m => fn ctxt => fn facts =>
diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/HOL/Filter.thy	Thu Nov 08 22:29:09 2018 +0100
@@ -1208,7 +1208,7 @@
 
   show "(\<Sqinter>i\<in>I. \<Sqinter>j\<in>J. A i \<times>\<^sub>F B j) \<le> (\<Sqinter>i\<in>I. A i) \<times>\<^sub>F (\<Sqinter>j\<in>J. B j)"
     by (fast intro: le_prod_filterI INF_greatest INF_lower2
-      order_trans[OF filtermap_INF] `i \<in> I` `j \<in> J`
+      order_trans[OF filtermap_INF] \<open>i \<in> I\<close> \<open>j \<in> J\<close>
       filtermap_fst_prod_filter filtermap_snd_prod_filter)
   show "(\<Sqinter>i\<in>I. A i) \<times>\<^sub>F (\<Sqinter>j\<in>J. B j) \<le> (\<Sqinter>i\<in>I. \<Sqinter>j\<in>J. A i \<times>\<^sub>F B j)"
     by (intro INF_greatest prod_filter_mono INF_lower)
diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/HOL/Library/Code_Lazy.thy
--- a/src/HOL/Library/Code_Lazy.thy	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/HOL/Library/Code_Lazy.thy	Thu Nov 08 22:29:09 2018 +0100
@@ -39,7 +39,7 @@
 
 ML_file "case_converter.ML"
 
-subsection \<open>The type @{text lazy}\<close>
+subsection \<open>The type \<open>lazy\<close>\<close>
 
 typedef 'a lazy = "UNIV :: 'a set" ..
 setup_lifting type_definition_lazy
diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/HOL/Library/IArray.thy
--- a/src/HOL/Library/IArray.thy	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/HOL/Library/IArray.thy	Thu Nov 08 22:29:09 2018 +0100
@@ -188,9 +188,9 @@
 
 subsection \<open>Code Generation for Haskell\<close>
 
-text \<open>We map @{typ "'a iarray"}s in Isabelle/HOL to @{text Data.Array.IArray.array}
-  in Haskell.  Performance mapping to @{text Data.Array.Unboxed.Array} and
-  @{text Data.Array.Array} is similar.\<close>
+text \<open>We map @{typ "'a iarray"}s in Isabelle/HOL to \<open>Data.Array.IArray.array\<close>
+  in Haskell.  Performance mapping to \<open>Data.Array.Unboxed.Array\<close> and
+  \<open>Data.Array.Array\<close> is similar.\<close>
 
 code_printing
   code_module "IArray" \<rightharpoonup> (Haskell) \<open>
diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/HOL/Library/Landau_Symbols.thy
--- a/src/HOL/Library/Landau_Symbols.thy	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/HOL/Library/Landau_Symbols.thy	Thu Nov 08 22:29:09 2018 +0100
@@ -4,7 +4,7 @@
 
   Landau symbols for reasoning about the asymptotic growth of functions. 
 *)
-section {* Definition of Landau symbols *}
+section \<open>Definition of Landau symbols\<close>
 
 theory Landau_Symbols
 imports 
@@ -16,14 +16,14 @@
   by (rule eventually_subst, erule eventually_rev_mp) simp
 
 
-subsection {* Definition of Landau symbols *}
+subsection \<open>Definition of Landau symbols\<close>
 
-text {*
+text \<open>
   Our Landau symbols are sign-oblivious, i.e. any function always has the same growth 
   as its absolute. This has the advantage of making some cancelling rules for sums nicer, but 
   introduces some problems in other places. Nevertheless, we found this definition more convenient
   to work with.
-*}
+\<close>
 
 definition bigo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
     ("(1O[_]'(_'))")
@@ -61,7 +61,7 @@
   "\<Theta>(g) \<equiv> bigtheta at_top g"
     
 
-text {* The following is a set of properties that all Landau symbols satisfy. *}
+text \<open>The following is a set of properties that all Landau symbols satisfy.\<close>
 
 named_theorems landau_divide_simps
 
@@ -290,11 +290,11 @@
 end
 
 
-text {* 
+text \<open>
   The symbols $O$ and $o$ and $\Omega$ and $\omega$ are dual, so for many rules, replacing $O$ with 
   $\Omega$, $o$ with $\omega$, and $\leq$ with $\geq$ in a theorem yields another valid theorem.
   The following locale captures this fact.
-*}
+\<close>
 
 locale landau_pair = 
   fixes L l :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
@@ -606,12 +606,12 @@
   } note A = this
   {
     fix c :: 'b and F and f :: "'a \<Rightarrow> 'b" assume "c \<noteq> 0"
-    from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] 
+    from \<open>c \<noteq> 0\<close> and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] 
       show "L F (\<lambda>x. c * f x) = L F f" by (intro equalityI big_subsetI) (simp_all add: field_simps)
   }
   {
     fix c :: 'b and F and f g :: "'a \<Rightarrow> 'b" assume "c \<noteq> 0"
-    from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]
+    from \<open>c \<noteq> 0\<close> and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]
       have "(\<lambda>x. c * f x) \<in> L F f" "f \<in> L F (\<lambda>x. c * f x)" by (simp_all add: field_simps)
     thus "((\<lambda>x. c * f x) \<in> L F g) = (f \<in> L F g)" by (intro iffI) (erule (1) big_trans)+
   }
@@ -689,13 +689,13 @@
   } note A = this
   {
     fix c :: 'b and f :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"
-    from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] 
+    from \<open>c \<noteq> 0\<close> and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] 
       show "l F (\<lambda>x. c * f x) = l F f" 
         by (intro equalityI small_subsetI) (simp_all add: field_simps)
   }
   {
     fix c :: 'b and f g :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"
-    from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]
+    from \<open>c \<noteq> 0\<close> and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]
       have "(\<lambda>x. c * f x) \<in> L F f" "f \<in> L F (\<lambda>x. c * f x)" by (simp_all add: field_simps)
     thus "((\<lambda>x. c * f x) \<in> l F g) = (f \<in> l F g)" by (intro iffI) (erule (1) big_small_trans)+
   }
@@ -763,7 +763,7 @@
 qed (auto simp: l_def lr_def eventually_filtermap l'_def eventually_sup intro: filter_leD)
 
 
-text {* These rules allow chaining of Landau symbol propositions in Isar with "also".*}
+text \<open>These rules allow chaining of Landau symbol propositions in Isar with "also".\<close>
 
 lemma big_mult_1:    "f \<in> L F (g) \<Longrightarrow> (\<lambda>_. 1) \<in> L F (h) \<Longrightarrow> f \<in> L F (\<lambda>x. g x * h x)"
   and big_mult_1':   "(\<lambda>_. 1) \<in> L F (g) \<Longrightarrow> f \<in> L F (h) \<Longrightarrow> f \<in> L F (\<lambda>x. g x * h x)"
@@ -1028,7 +1028,7 @@
 qed
 
 
-subsection {* Landau symbols and limits *}
+subsection \<open>Landau symbols and limits\<close>
 
 lemma bigoI_tendsto_norm:
   fixes f g
@@ -1073,7 +1073,7 @@
     with c_not_0 show "c/2 > 0" by simp
     from lim have ev: "\<And>\<epsilon>. \<epsilon> > 0 \<Longrightarrow> eventually (\<lambda>x. norm (norm (f x / g x) - c) < \<epsilon>) F"
       by (subst (asm) tendsto_iff) (simp add: dist_real_def)
-    from ev[OF `c/2 > 0`] show "eventually (\<lambda>x. (norm (f x)) \<ge> c/2 * (norm (g x))) F"
+    from ev[OF \<open>c/2 > 0\<close>] show "eventually (\<lambda>x. (norm (f x)) \<ge> c/2 * (norm (g x))) F"
     proof (eventually_elim)
       fix x assume B: "norm (norm (f x / g x) - c) < c / 2"
       from B have g: "g x \<noteq> 0" by auto
@@ -1523,16 +1523,16 @@
     assume "p < q"
     hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A
       by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
-    with `p < q` show ?thesis by auto
+    with \<open>p < q\<close> show ?thesis by auto
   next
     assume "p = q"
     hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" by (auto intro!: bigthetaD1)
-    with B `p = q` show ?thesis by auto
+    with B \<open>p = q\<close> show ?thesis by auto
   next
     assume "p > q"
     hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" using assms A
       by (auto intro!: smalloI_tendsto tendsto_neg_powr landau_o.small_imp_big simp flip: powr_diff)
-    with B `p > q` show ?thesis by auto
+    with B \<open>p > q\<close> show ?thesis by auto
   qed
 qed
 
@@ -1554,16 +1554,16 @@
     assume "p < q"
     hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A
       by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
-    with `p < q` show ?thesis by (auto intro: landau_o.small_imp_big)
+    with \<open>p < q\<close> show ?thesis by (auto intro: landau_o.small_imp_big)
   next
     assume "p = q"
     hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" by (auto intro!: bigthetaD1)
-    with B `p = q` show ?thesis by auto
+    with B \<open>p = q\<close> show ?thesis by auto
   next
     assume "p > q"
     hence "(\<lambda>x. g x powr q) \<in> o[F](\<lambda>x. g x powr p)" using assms A
       by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
-    with B `p > q` show ?thesis by (auto intro: landau_o.small_imp_big)
+    with B \<open>p > q\<close> show ?thesis by (auto intro: landau_o.small_imp_big)
   qed
 qed
 
diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/HOL/Limits.thy	Thu Nov 08 22:29:09 2018 +0100
@@ -173,7 +173,7 @@
     unfolding Bfun_def by fast
   with assms(1) have "eventually (\<lambda>n. norm (f n) \<le> K) sequentially"
     by (fast elim: eventually_elim2 order_trans)
-  with `0 < K` show "Bseq f"
+  with \<open>0 < K\<close> show "Bseq f"
     unfolding Bfun_def by fast
 qed
 
diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/HOL/ROOT
--- a/src/HOL/ROOT	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/HOL/ROOT	Thu Nov 08 22:29:09 2018 +0100
@@ -1,9 +1,9 @@
 chapter HOL
 
 session HOL (main) = Pure +
-  description {*
+  description \<open>
     Classical Higher-order Logic.
-  *}
+\<close>
   options [strict_facts]
   theories
     Main (global)
@@ -13,9 +13,9 @@
     "root.tex"
 
 session "HOL-Proofs" (timing) = Pure +
-  description {*
+  description \<open>
     HOL-Main with explicit proof terms.
-  *}
+\<close>
   options [quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0, parallel_limit = 500]
   sessions
     "HOL-Library"
@@ -23,9 +23,9 @@
     "HOL-Library.Realizers"
 
 session "HOL-Library" (main timing) in Library = HOL +
-  description {*
+  description \<open>
     Classical Higher-order Logic -- batteries included.
-  *}
+\<close>
   theories
     Library
     (*conflicting type class instantiations and dependent applications*)
@@ -100,7 +100,7 @@
     "style.sty"
 
 session "HOL-Hahn_Banach" in Hahn_Banach = "HOL-Library" +
-  description {*
+  description \<open>
     Author:     Gertrud Bauer, TU Munich
 
     The Hahn-Banach theorem for real vector spaces.
@@ -116,7 +116,7 @@
     The theorem says, that every continous linearform, defined on arbitrary
     subspaces (not only one-dimensional subspaces), can be extended to a
     continous linearform on the whole vectorspace.
-  *}
+\<close>
   sessions
     "HOL-Analysis"
   theories
@@ -124,7 +124,7 @@
   document_files "root.bib" "root.tex"
 
 session "HOL-Induct" in Induct = "HOL-Library" +
-  description {*
+  description \<open>
     Examples of (Co)Inductive Definitions.
 
     Comb proves the Church-Rosser theorem for combinators (see
@@ -139,7 +139,7 @@
 
     Exp demonstrates the use of iterated inductive definitions to reason about
     mutually recursive relations.
-  *}
+\<close>
   theories [quick_and_dirty]
     Common_Patterns
   theories
@@ -193,7 +193,7 @@
   document_files "root.bib" "root.tex"
 
 session "HOL-IMPP" in IMPP = HOL +
-  description {*
+  description \<open>
     Author:     David von Oheimb
     Copyright   1999 TUM
 
@@ -202,7 +202,7 @@
     This is an extension of IMP with local variables and mutually recursive
     procedures. For documentation see "Hoare Logic for Mutual Recursion and
     Local Variables" (https://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
-  *}
+\<close>
   theories EvenOdd
 
 session "HOL-Data_Structures" (timing) in Data_Structures = HOL +
@@ -233,10 +233,10 @@
   theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
 
 session "HOL-Number_Theory" (main timing) in Number_Theory = "HOL-Computational_Algebra" +
-  description {*
+  description \<open>
     Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
     Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.
-  *}
+\<close>
   sessions
     "HOL-Algebra"
   theories
@@ -245,18 +245,18 @@
     "root.tex"
 
 session "HOL-Hoare" in Hoare = HOL +
-  description {*
+  description \<open>
     Verification of imperative programs (verification conditions are generated
     automatically from pre/post conditions and loop invariants).
-  *}
+\<close>
   theories Hoare
   document_files "root.bib" "root.tex"
 
 session "HOL-Hoare_Parallel" (timing) in Hoare_Parallel = HOL +
-  description {*
+  description \<open>
     Verification of shared-variable imperative programs a la Owicki-Gries.
     (verification conditions are generated automatically).
-  *}
+\<close>
   theories Hoare_Parallel
   document_files "root.bib" "root.tex"
 
@@ -282,12 +282,12 @@
     Code_Test_SMLNJ
 
 session "HOL-Metis_Examples" (timing) in Metis_Examples = "HOL-Library" +
-  description {*
+  description \<open>
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Jasmin Blanchette, TU Muenchen
 
     Testing Metis and Sledgehammer.
-  *}
+\<close>
   sessions
     "HOL-Decision_Procs"
   theories
@@ -302,18 +302,18 @@
     Sets
 
 session "HOL-Nitpick_Examples" in Nitpick_Examples = "HOL-Library" +
-  description {*
+  description \<open>
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2009
-  *}
+\<close>
   theories [quick_and_dirty] Nitpick_Examples
 
 session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" +
-  description {*
+  description \<open>
     Author: Clemens Ballarin, started 24 September 1999, and many others
 
     The Isabelle Algebraic Library.
-  *}
+\<close>
   theories
     (* Orders and Lattices *)
     Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)
@@ -332,9 +332,9 @@
   document_files "root.bib" "root.tex"
 
 session "HOL-Auth" (timing) in Auth = "HOL-Library" +
-  description {*
+  description \<open>
     A new approach to verifying authentication protocols.
-  *}
+\<close>
   theories
     Auth_Shared
     Auth_Public
@@ -344,12 +344,12 @@
   document_files "root.tex"
 
 session "HOL-UNITY" (timing) in UNITY = "HOL-Auth" +
-  description {*
+  description \<open>
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
     Verifying security protocols using Chandy and Misra's UNITY formalism.
-  *}
+\<close>
   theories
     (*Basic meta-theory*)
     UNITY_Main
@@ -404,9 +404,9 @@
   document_files "root.bib" "root.tex"
 
 session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" +
-  description {*
+  description \<open>
     Various decision procedures, typically involving reflection.
-  *}
+\<close>
   theories
     Decision_Procs
 
@@ -419,9 +419,9 @@
     XML_Data
 
 session "HOL-Proofs-Extraction" (timing) in "Proofs/Extraction" = "HOL-Proofs" +
-  description {*
+  description \<open>
     Examples for program extraction in Higher-Order Logic.
-  *}
+\<close>
   options [parallel_proofs = 0, quick_and_dirty = false]
   sessions
     "HOL-Computational_Algebra"
@@ -434,7 +434,7 @@
   document_files "root.bib" "root.tex"
 
 session "HOL-Proofs-Lambda" (timing) in "Proofs/Lambda" = "HOL-Proofs" +
-  description {*
+  description \<open>
     Lambda Calculus in de Bruijn's Notation.
 
     This session defines lambda-calculus terms with de Bruijn indixes and
@@ -442,7 +442,7 @@
 
     The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
     theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
-  *}
+\<close>
   options [print_mode = "no_brackets",
     parallel_proofs = 0, quick_and_dirty = false]
   sessions
@@ -455,7 +455,7 @@
   document_files "root.bib" "root.tex"
 
 session "HOL-Prolog" in Prolog = HOL +
-  description {*
+  description \<open>
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
 
     A bare-bones implementation of Lambda-Prolog.
@@ -463,15 +463,15 @@
     This is a simple exploratory implementation of Lambda-Prolog in HOL,
     including some minimal examples (in Test.thy) and a more typical example of
     a little functional language and its type system.
-  *}
+\<close>
   theories Test Type
 
 session "HOL-MicroJava" (timing) in MicroJava = "HOL-Library" +
-  description {*
+  description \<open>
     Formalization of a fragment of Java, together with a corresponding virtual
     machine and a specification of its bytecode verifier and a lightweight
     bytecode verifier, including proofs of type-safety.
-  *}
+\<close>
   sessions
     "HOL-Eisbach"
   theories
@@ -482,9 +482,9 @@
     "root.tex"
 
 session "HOL-NanoJava" in NanoJava = HOL +
-  description {*
+  description \<open>
     Hoare Logic for a tiny fragment of Java.
-  *}
+\<close>
   theories Example
   document_files "root.bib" "root.tex"
 
@@ -498,7 +498,7 @@
   document_files "root.tex"
 
 session "HOL-IOA" in IOA = HOL +
-  description {*
+  description \<open>
     Author:     Tobias Nipkow and Konrad Slind and Olaf Müller
     Copyright   1994--1996  TU Muenchen
 
@@ -524,22 +524,22 @@
     organization={Aarhus University, BRICS report},
     year=1995}
     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
-  *}
+\<close>
   theories Solve
 
 session "HOL-Lattice" in Lattice = HOL +
-  description {*
+  description \<open>
     Author:     Markus Wenzel, TU Muenchen
 
     Basic theory of lattices and orders.
-  *}
+\<close>
   theories CompleteLattice
   document_files "root.tex"
 
 session "HOL-ex" (timing) in ex = "HOL-Number_Theory" +
-  description {*
+  description \<open>
     Miscellaneous examples for Higher-Order Logic.
-  *}
+\<close>
   theories
     Adhoc_Overloading_Examples
     Antiquote
@@ -634,9 +634,9 @@
     Meson_Test
 
 session "HOL-Isar_Examples" in Isar_Examples = "HOL-Computational_Algebra" +
-  description {*
+  description \<open>
     Miscellaneous Isabelle/Isar examples.
-  *}
+\<close>
   options [quick_and_dirty]
   theories
     Knaster_Tarski
@@ -661,9 +661,9 @@
     "root.tex"
 
 session "HOL-Eisbach" in Eisbach = HOL +
-  description {*
+  description \<open>
     The Eisbach proof method language and "match" method.
-  *}
+\<close>
   sessions
     FOL
   theories
@@ -673,24 +673,24 @@
     Examples_FOL
 
 session "HOL-SET_Protocol" (timing) in SET_Protocol = "HOL-Library" +
-  description {*
+  description \<open>
     Verification of the SET Protocol.
-  *}
+\<close>
   theories
     SET_Protocol
   document_files "root.tex"
 
 session "HOL-Matrix_LP" in Matrix_LP = "HOL-Library" +
-  description {*
+  description \<open>
     Two-dimensional matrices and linear programming.
-  *}
+\<close>
   theories Cplex
   document_files "root.tex"
 
 session "HOL-TLA" in TLA = HOL +
-  description {*
+  description \<open>
     Lamport's Temporal Logic of Actions.
-  *}
+\<close>
   theories TLA
 
 session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
@@ -703,13 +703,13 @@
   theories MemoryImplementation
 
 session "HOL-TPTP" in TPTP = "HOL-Library" +
-  description {*
+  description \<open>
     Author:     Jasmin Blanchette, TU Muenchen
     Author:     Nik Sultana, University of Cambridge
     Copyright   2011
 
     TPTP-related extensions.
-  *}
+\<close>
   theories
     ATP_Theory_Export
     MaSh_Eval
@@ -760,9 +760,9 @@
     VC_Condition
 
 session "HOL-Cardinals" (timing) in Cardinals = "HOL-Library" +
-  description {*
+  description \<open>
     Ordinals and Cardinals, Full Theories.
-  *}
+\<close>
   theories
     Cardinals
     Bounded_Set
@@ -772,9 +772,9 @@
     "root.bib"
 
 session "HOL-Datatype_Examples" (timing) in Datatype_Examples = "HOL-Library" +
-  description {*
+  description \<open>
     (Co)datatype Examples.
-  *}
+\<close>
   theories
     Compat
     Lambda_Term
@@ -792,9 +792,9 @@
     Misc_Primrec
 
 session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" +
-  description {*
+  description \<open>
     Corecursion Examples.
-  *}
+\<close>
   theories
     LFilter
     Paper_Examples
@@ -828,9 +828,9 @@
   document_files "root.tex"
 
 session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = "HOL-Computational_Algebra" +
-  description {*
+  description \<open>
     Nonstandard analysis.
-  *}
+\<close>
   theories
     Nonstandard_Analysis
   document_files "root.tex"
@@ -911,9 +911,9 @@
     Quickcheck_Narrowing_Examples
 
 session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Algebra" +
-  description {*
+  description \<open>
     Author:     Cezary Kaliszyk and Christian Urban
-  *}
+\<close>
   theories
     DList
     Quotient_FSet
@@ -949,9 +949,9 @@
     Reg_Exp_Example
 
 session "HOL-Types_To_Sets" in Types_To_Sets = HOL +
-  description {*
+  description \<open>
     Experimental extension of Higher-Order Logic to allow translation of types to sets.
-  *}
+\<close>
   theories
     Types_To_Sets
     "Examples/Prerequisites"
@@ -960,12 +960,12 @@
     "Examples/Linear_Algebra_On"
 
 session HOLCF (main timing) in HOLCF = HOL +
-  description {*
+  description \<open>
     Author:     Franz Regensburger
     Author:     Brian Huffman
 
     HOLCF -- a semantic extension of HOL by the LCF logic.
-  *}
+\<close>
   sessions
     "HOL-Library"
   theories
@@ -985,11 +985,11 @@
     HOL_Cpo
 
 session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
-  description {*
+  description \<open>
     IMP -- A WHILE-language and its Semantics.
 
     This is the HOLCF-based denotational semantics of a simple WHILE-language.
-  *}
+\<close>
   sessions
     "HOL-IMP"
   theories
@@ -1000,9 +1000,9 @@
     "root.bib"
 
 session "HOLCF-ex" in "HOLCF/ex" = "HOLCF-Library" +
-  description {*
+  description \<open>
     Miscellaneous examples for HOLCF.
-  *}
+\<close>
   theories
     Dnat
     Dagstuhl
@@ -1017,7 +1017,7 @@
     Pattern_Match
 
 session "HOLCF-FOCUS" in "HOLCF/FOCUS" = "HOLCF-Library" +
-  description {*
+  description \<open>
     FOCUS: a theory of stream-processing functions Isabelle/HOLCF.
 
     For introductions to FOCUS, see
@@ -1030,14 +1030,14 @@
 
     "Specification and Development of Interactive Systems: Focus on Streams,
     Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
-  *}
+\<close>
   theories
     Fstreams
     FOCUS
     Buffer_adm
 
 session IOA (timing) in "HOLCF/IOA" = HOLCF +
-  description {*
+  description \<open>
     Author:     Olaf Mueller
     Copyright   1997 TU München
 
@@ -1046,40 +1046,40 @@
     The distribution contains simulation relations, temporal logic, and an
     abstraction theory. Everything is based upon a domain-theoretic model of
     finite and infinite sequences.
-  *}
+\<close>
   theories Abstraction
 
 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
-  description {*
+  description \<open>
     Author:     Olaf Mueller
 
     The Alternating Bit Protocol performed in I/O-Automata.
-  *}
+\<close>
   theories
     Correctness
     Spec
 
 session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
-  description {*
+  description \<open>
     Author:     Tobias Nipkow & Konrad Slind
 
     A network transmission protocol, performed in the
     I/O automata formalization by Olaf Mueller.
-  *}
+\<close>
   theories Correctness
 
 session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
-  description {*
+  description \<open>
     Author:     Olaf Mueller
 
     Memory storage case study.
-  *}
+\<close>
   theories Correctness
 
 session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
-  description {*
+  description \<open>
     Author:     Olaf Mueller
-  *}
+\<close>
   theories
     TrivEx
     TrivEx2
diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/HOL/String.thy
--- a/src/HOL/String.thy	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/HOL/String.thy	Thu Nov 08 22:29:09 2018 +0100
@@ -398,16 +398,16 @@
 text \<open>
   Logical ground representations for literals are:
 
-  \<^enum> @{text 0} for the empty literal;
+  \<^enum> \<open>0\<close> for the empty literal;
 
-  \<^enum> @{text "Literal b0 \<dots> b6 s"} for a literal starting with one
+  \<^enum> \<open>Literal b0 \<dots> b6 s\<close> for a literal starting with one
     character and continued by another literal.
 
   Syntactic representations for literals are:
 
-  \<^enum> Printable text as string prefixed with @{text STR};
+  \<^enum> Printable text as string prefixed with \<open>STR\<close>;
 
-  \<^enum> A single ascii value as numerical hexadecimal value prefixed with @{text STR}.
+  \<^enum> A single ascii value as numerical hexadecimal value prefixed with \<open>STR\<close>.
 \<close>
 
 instantiation String.literal :: zero
diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/HOL/Transcendental.thy	Thu Nov 08 22:29:09 2018 +0100
@@ -4009,7 +4009,7 @@
   shows "0 < sin (pi / real n)"
   by (rule sin_gt_zero) (use assms in \<open>simp_all add: divide_simps\<close>)
 
-text\<open>Proof resembles that of @{text cos_is_zero} but with @{term pi} for the upper bound\<close>
+text\<open>Proof resembles that of \<open>cos_is_zero\<close> but with @{term pi} for the upper bound\<close>
 lemma cos_total:
   assumes y: "-1 \<le> y" "y \<le> 1"
   shows "\<exists>!x. 0 \<le> x \<and> x \<le> pi \<and> cos x = y"
diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/LCF/ROOT
--- a/src/LCF/ROOT	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/LCF/ROOT	Thu Nov 08 22:29:09 2018 +0100
@@ -1,7 +1,7 @@
 chapter LCF
 
 session LCF = Pure +
-  description {*
+  description \<open>
     Author:     Tobias Nipkow
     Copyright   1992  University of Cambridge
 
@@ -9,7 +9,7 @@
 
     Useful references on LCF: Lawrence C. Paulson,
     Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
-  *}
+\<close>
   sessions
     FOL
   theories
diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/Pure/ROOT
--- a/src/Pure/ROOT	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/Pure/ROOT	Thu Nov 08 22:29:09 2018 +0100
@@ -1,9 +1,9 @@
 chapter Pure
 
 session Pure =
-  description {*
+  description \<open>
     The Pure logical framework
-  *}
+\<close>
   options [threads = 1, export_theory]
   theories
     Pure (global)
diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/Sequents/ROOT
--- a/src/Sequents/ROOT	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/Sequents/ROOT	Thu Nov 08 22:29:09 2018 +0100
@@ -1,7 +1,7 @@
 chapter Sequents
 
 session Sequents = Pure +
-  description {*
+  description \<open>
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
@@ -36,7 +36,7 @@
 
     S. Kalvala and V. de Paiva, Linear Logic in Isabelle (in TR 379, University
     of Cambridge Computer Lab, 1995, ed L. Paulson)
-  *}
+\<close>
   theories
     LK
     ILL
diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/ZF/ROOT
--- a/src/ZF/ROOT	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/ZF/ROOT	Thu Nov 08 22:29:09 2018 +0100
@@ -1,7 +1,7 @@
 chapter ZF
 
 session ZF (main timing) = Pure +
-  description {*
+  description \<open>
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 
@@ -41,7 +41,7 @@
 
     Kenneth Kunen, Set Theory: An Introduction to Independence Proofs,
     (North-Holland, 1980)
-  *}
+\<close>
   sessions
     FOL
   theories
@@ -50,7 +50,7 @@
   document_files "root.tex"
 
 session "ZF-AC" in AC = ZF +
-  description {*
+  description \<open>
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 
@@ -63,7 +63,7 @@
     http://www.cl.cam.ac.uk/Research/Reports/TR377-lcp-mechanising-set-theory.ps.gz
     "Mechanizing Set Theory", by Paulson and Grabczewski, describes both this
     development and ZF's theories of cardinals.
-  *}
+\<close>
   theories
     WO6_WO1
     WO1_WO7
@@ -78,7 +78,7 @@
   document_files "root.tex" "root.bib"
 
 session "ZF-Coind" in Coind = ZF +
-  description {*
+  description \<open>
     Author:     Jacob Frost, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 
@@ -99,11 +99,11 @@
         Jacob Frost, A Case Study of Co_induction in Isabelle
         Report, Computer Lab, University of Cambridge (1995).
         http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz
-  *}
+\<close>
   theories ECR
 
 session "ZF-Constructible" in Constructible = ZF +
-  description {*
+  description \<open>
     Relative Consistency of the Axiom of Choice:
     Inner Models, Absoluteness and Consistency Proofs.
 
@@ -121,7 +121,7 @@
 
     A paper describing this development is
     http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf
-  *}
+\<close>
   theories
     DPow_absolute
     AC_in_L
@@ -129,7 +129,7 @@
   document_files "root.tex" "root.bib"
 
 session "ZF-IMP" in IMP = ZF +
-  description {*
+  description \<open>
     Author:     Heiko Loetzbeyer & Robert Sandner, TUM
     Copyright   1994 TUM
 
@@ -141,19 +141,19 @@
 
     Glynn Winskel. The Formal Semantics of Programming Languages.
     MIT Press, 1993.
-  *}
+\<close>
   theories Equiv
   document_files
     "root.tex"
     "root.bib"
 
 session "ZF-Induct" in Induct = ZF +
-  description {*
+  description \<open>
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2001  University of Cambridge
 
     Inductive definitions.
-  *}
+\<close>
   theories
     (** Datatypes **)
     Datatypes       (*sample datatypes*)
@@ -181,7 +181,7 @@
     "root.tex"
 
 session "ZF-Resid" in Resid = ZF +
-  description {*
+  description \<open>
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 
@@ -196,16 +196,16 @@
     See Rasmussen's report: The Church-Rosser Theorem in Isabelle: A Proof
     Porting Experiment.
     http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz
-  *}
+\<close>
   theories Confluence
 
 session "ZF-UNITY" (timing) in UNITY = "ZF-Induct" +
-  description {*
+  description \<open>
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
     ZF/UNITY proofs.
-  *}
+\<close>
   theories
     (*Simple examples: no composition*)
     Mutex
@@ -217,7 +217,7 @@
     Distributor Merge ClientImpl AllocImpl
 
 session "ZF-ex" in ex = ZF +
-  description {*
+  description \<open>
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
@@ -231,7 +231,7 @@
     describes the theoretical foundations of datatypes while
     href="http://www.cl.cam.ac.uk/Research/Reports/TR320-lcp-isabelle-ind-defs.dvi.gz
     describes the package that automates their declaration.
-  *}
+\<close>
   theories
     misc
     Ring             (*abstract algebra*)