# HG changeset patch
# User wenzelm
# Date 1446716389 -3600
# Node ID a9599d3d761002c1877775ed1bfee705f56dd706
# Parent  f06e5a5a4b46ba88cd83dbdba6ce8cf12ea85f02
isabelle update_cartouches -c -t;

diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/AList.thy
--- a/src/HOL/Library/AList.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/AList.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -18,7 +18,7 @@
   to establish the invariant, e.g. for inductive proofs.
 \<close>
 
-subsection \<open>@{text update} and @{text updates}\<close>
+subsection \<open>\<open>update\<close> and \<open>updates\<close>\<close>
 
 qualified primrec update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
@@ -163,7 +163,7 @@
   by (induct xs arbitrary: ys al) (auto split: list.splits)
 
 
-subsection \<open>@{text delete}\<close>
+subsection \<open>\<open>delete\<close>\<close>
 
 qualified definition delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   where delete_eq: "delete k = filter (\<lambda>(k', _). k \<noteq> k')"
@@ -215,7 +215,7 @@
   by (simp add: delete_eq)
 
 
-subsection \<open>@{text update_with_aux} and @{text delete_aux}\<close>
+subsection \<open>\<open>update_with_aux\<close> and \<open>delete_aux\<close>\<close>
 
 qualified primrec update_with_aux :: "'val \<Rightarrow> 'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
@@ -296,7 +296,7 @@
 by(cases ts)(auto split: split_if_asm)
 
 
-subsection \<open>@{text restrict}\<close>
+subsection \<open>\<open>restrict\<close>\<close>
 
 qualified definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   where restrict_eq: "restrict A = filter (\<lambda>(k, v). k \<in> A)"
@@ -380,7 +380,7 @@
   by (induct ps) auto
 
 
-subsection \<open>@{text clearjunk}\<close>
+subsection \<open>\<open>clearjunk\<close>\<close>
 
 qualified function clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
@@ -464,7 +464,7 @@
     (simp_all add: clearjunk_delete delete_map assms)
 
 
-subsection \<open>@{text map_ran}\<close>
+subsection \<open>\<open>map_ran\<close>\<close>
 
 definition map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   where "map_ran f = map (\<lambda>(k, v). (k, f k v))"
@@ -490,7 +490,7 @@
   by (simp add: map_ran_def split_def clearjunk_map)
 
 
-subsection \<open>@{text merge}\<close>
+subsection \<open>\<open>merge\<close>\<close>
 
 qualified definition merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   where "merge qs ps = foldr (\<lambda>(k, v). update k v) ps qs"
@@ -558,7 +558,7 @@
   by (simp add: merge_conv')
 
 
-subsection \<open>@{text compose}\<close>
+subsection \<open>\<open>compose\<close>\<close>
 
 qualified function compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list"
 where
@@ -723,7 +723,7 @@
   by (simp add: compose_conv map_comp_None_iff)
 
 
-subsection \<open>@{text map_entry}\<close>
+subsection \<open>\<open>map_entry\<close>\<close>
 
 qualified fun map_entry :: "'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
@@ -745,7 +745,7 @@
   using assms by (induct xs) (auto simp add: dom_map_entry)
 
 
-subsection \<open>@{text map_default}\<close>
+subsection \<open>\<open>map_default\<close>\<close>
 
 fun map_default :: "'key \<Rightarrow> 'val \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/BigO.thy
--- a/src/HOL/Library/BigO.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/BigO.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -16,20 +16,20 @@
 
 The main changes in this version are as follows:
 \begin{itemize}
-\item We have eliminated the @{text O} operator on sets. (Most uses of this seem
+\item We have eliminated the \<open>O\<close> operator on sets. (Most uses of this seem
   to be inessential.)
-\item We no longer use @{text "+"} as output syntax for @{text "+o"}
-\item Lemmas involving @{text "sumr"} have been replaced by more general lemmas
-  involving `@{text "setsum"}.
+\item We no longer use \<open>+\<close> as output syntax for \<open>+o\<close>
+\item Lemmas involving \<open>sumr\<close> have been replaced by more general lemmas
+  involving `\<open>setsum\<close>.
 \item The library has been expanded, with e.g.~support for expressions of
-  the form @{text "f < g + O(h)"}.
+  the form \<open>f < g + O(h)\<close>.
 \end{itemize}
 
 Note also since the Big O library includes rules that demonstrate set
 inclusion, to use the automated reasoners effectively with the library
-one should redeclare the theorem @{text "subsetI"} as an intro rule,
-rather than as an @{text "intro!"} rule, for example, using
-\isa{\isakeyword{declare}}~@{text "subsetI [del, intro]"}.
+one should redeclare the theorem \<open>subsetI\<close> as an intro rule,
+rather than as an \<open>intro!\<close> rule, for example, using
+\isa{\isakeyword{declare}}~\<open>subsetI [del, intro]\<close>.
 \<close>
 
 subsection \<open>Definitions\<close>
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Cardinality.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -211,7 +211,7 @@
   fixes card_UNIV :: "'a card_UNIV"
   assumes card_UNIV: "card_UNIV = Phantom('a) CARD('a)"
 
-subsection \<open>Instantiations for @{text "card_UNIV"}\<close>
+subsection \<open>Instantiations for \<open>card_UNIV\<close>\<close>
 
 instantiation nat :: card_UNIV begin
 definition "finite_UNIV = Phantom(nat) False"
@@ -534,7 +534,7 @@
      (\<lambda>_. List.coset xs \<subseteq> set ys))"
 by simp
 
-notepad begin -- "test code setup"
+notepad begin \<comment> "test code setup"
 have "List.coset [True] = set [False] \<and> 
       List.coset [] \<subseteq> List.set [True, False] \<and> 
       finite (List.coset [True])"
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Code_Char.thy
--- a/src/HOL/Library/Code_Char.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Code_Char.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -107,7 +107,7 @@
 |  constant "Orderings.less_eq :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
     (SML) "!((_ : string) <= _)"
     and (OCaml) "!((_ : string) <= _)"
-    -- \<open>Order operations for @{typ String.literal} work in Haskell only 
+    \<comment> \<open>Order operations for @{typ String.literal} work in Haskell only 
           if no type class instance needs to be generated, because String = [Char] in Haskell
           and @{typ "char list"} need not have the same order as @{typ String.literal}.\<close>
     and (Haskell) infix 4 "<="
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Code_Target_Nat.thy
--- a/src/HOL/Library/Code_Target_Nat.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Code_Target_Nat.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -135,7 +135,7 @@
   including integer.lifting by transfer auto
 
 lemma term_of_nat_code [code]:
-  -- \<open>Use @{term Code_Numeral.nat_of_integer} in term reconstruction
+  \<comment> \<open>Use @{term Code_Numeral.nat_of_integer} in term reconstruction
         instead of @{term Code_Target_Nat.Nat} such that reconstructed
         terms can be fed back to the code generator\<close>
   "term_of_class.term_of n =
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Code_Test.thy
--- a/src/HOL/Library/Code_Test.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Code_Test.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -131,7 +131,7 @@
   "xml_of_term (Code_Evaluation.Const x ty) = [xml.tagged (STR ''0'') (Some x) (xml_of_typ ty)]"
   "xml_of_term (Code_Evaluation.App t1 t2)  = [xml.tagged (STR ''5'') None [xml.node (xml_of_term t1), xml.node (xml_of_term t2)]]"
   "xml_of_term (Code_Evaluation.Abs x ty t) = [xml.tagged (STR ''4'') (Some x) [xml.node (xml_of_typ ty), xml.node (xml_of_term t)]]"
-  -- \<open>
+  \<comment> \<open>
     FIXME: @{const Code_Evaluation.Free} is used only in @{theory Quickcheck_Narrowing} to represent
     uninstantiated parameters in constructors. Here, we always translate them to @{ML Free} variables.
 \<close>
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/ContNotDenum.thy
--- a/src/HOL/Library/ContNotDenum.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/ContNotDenum.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -15,8 +15,8 @@
 uncountable. It is formalised in the Isabelle/Isar theorem proving
 system.
 
-{\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other
-words, there does not exist a function @{text "f: \<nat> \<Rightarrow> \<real>"} such that f is
+{\em Theorem:} The Continuum \<open>\<real>\<close> is not denumerable. In other
+words, there does not exist a function \<open>f: \<nat> \<Rightarrow> \<real>\<close> such that f is
 surjective.
 
 {\em Outline:} An elegant informal proof of this result uses Cantor's
@@ -26,8 +26,7 @@
 completeness of the Real numbers and is the foundation for our
 argument. Informally it states that an intersection of countable
 closed intervals (where each successive interval is a subset of the
-last) is non-empty. We then assume a surjective function @{text
-"f: \<nat> \<Rightarrow> \<real>"} exists and find a real x such that x is not in the range of f
+last) is non-empty. We then assume a surjective function \<open>f: \<nat> \<Rightarrow> \<real>\<close> exists and find a real x such that x is not in the range of f
 by generating a sequence of closed intervals then using the NIP.\<close>
 
 theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)"
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Convex.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -883,7 +883,7 @@
   fix t x y :: real
   assume t: "t > 0" "t < 1" and xy: "x \<in> A" "y \<in> A" "x < y"
   def z \<equiv> "(1 - t) * x + t * y"
-  with `connected A` and xy have ivl: "{x..y} \<subseteq> A" using connected_contains_Icc by blast
+  with \<open>connected A\<close> and xy have ivl: "{x..y} \<subseteq> A" using connected_contains_Icc by blast
   
   from xy t have xz: "z > x" by (simp add: z_def algebra_simps)
   have "y - z = (1 - t) * (y - x)" by (simp add: z_def algebra_simps)
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Countable_Set_Type.thy
--- a/src/HOL/Library/Countable_Set_Type.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Countable_Set_Type.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -369,11 +369,11 @@
 
 subsection \<open>Additional lemmas\<close>
 
-subsubsection \<open>@{text cempty}\<close>
+subsubsection \<open>\<open>cempty\<close>\<close>
 
 lemma cemptyE [elim!]: "cin a cempty \<Longrightarrow> P" by simp
 
-subsubsection \<open>@{text cinsert}\<close>
+subsubsection \<open>\<open>cinsert\<close>\<close>
 
 lemma countable_insert_iff: "countable (insert x A) \<longleftrightarrow> countable A"
 by (metis Diff_eq_empty_iff countable_empty countable_insert subset_insertI uncountable_minus_countable)
@@ -386,7 +386,7 @@
 lemma mk_disjoint_cinsert: "cin a A \<Longrightarrow> \<exists>B. A = cinsert a B \<and> \<not> cin a B"
   by (rule exI[where x = "cDiff A (csingle a)"]) blast
 
-subsubsection \<open>@{text cimage}\<close>
+subsubsection \<open>\<open>cimage\<close>\<close>
 
 lemma subset_cimage_iff: "csubset_eq B (cimage f A) \<longleftrightarrow> (\<exists>AA. csubset_eq AA A \<and> B = cimage f AA)"
 by transfer (metis countable_subset image_mono mem_Collect_eq subset_imageE) 
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/DAList.thy
--- a/src/HOL/Library/DAList.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/DAList.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -17,7 +17,7 @@
   by (induct xs) auto
 
 
-subsection \<open>Type @{text "('key, 'value) alist" }\<close>
+subsection \<open>Type \<open>('key, 'value) alist\<close>\<close>
 
 typedef ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. (distinct \<circ> map fst) xs}"
   morphisms impl_of Alist
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/DAList_Multiset.thy
--- a/src/HOL/Library/DAList_Multiset.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/DAList_Multiset.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -206,8 +206,8 @@
 lemma mset_eq [code]: "HOL.equal (m1::'a::equal multiset) m2 \<longleftrightarrow> m1 \<le># m2 \<and> m2 \<le># m1"
   by (metis equal_multiset_def subset_mset.eq_iff)
 
-text \<open>By default the code for @{text "<"} is @{prop"xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> xs = ys"}.
-With equality implemented by @{text"\<le>"}, this leads to three calls of  @{text"\<le>"}.
+text \<open>By default the code for \<open><\<close> is @{prop"xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> xs = ys"}.
+With equality implemented by \<open>\<le>\<close>, this leads to three calls of  \<open>\<le>\<close>.
 Here is a more efficient version:\<close>
 lemma mset_less[code]: "xs <# (ys :: 'a multiset) \<longleftrightarrow> xs \<le># ys \<and> \<not> ys \<le># xs"
   by (rule subset_mset.less_le_not_le)
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Debug.thy
--- a/src/HOL/Library/Debug.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Debug.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -36,7 +36,7 @@
 
 code_printing
   constant Debug.trace \<rightharpoonup> (Eval) "Output.tracing"
-| constant Debug.flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" -- \<open>note indirection via antiquotation\<close>
+| constant Debug.flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" \<comment> \<open>note indirection via antiquotation\<close>
 | constant Debug.timing \<rightharpoonup> (Eval) "Timing.timeap'_msg"
 
 code_reserved Eval Output Timing
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -14,7 +14,7 @@
 text \<open>
 
 This should be part of @{theory Extended_Nat} or @{theory Order_Continuity}, but then the
-AFP-entry @{text "Jinja_Thread"} fails, as it does overload certain named from @{theory Complex_Main}.
+AFP-entry \<open>Jinja_Thread\<close> fails, as it does overload certain named from @{theory Complex_Main}.
 
 \<close>
 
@@ -3613,7 +3613,7 @@
   shows "inverse -- x --> inverse x"
 proof (cases x)
   case (real r)
-  with `0 < x` have **: "(\<lambda>x. ereal (inverse x)) -- r --> ereal (inverse r)"
+  with \<open>0 < x\<close> have **: "(\<lambda>x. ereal (inverse x)) -- r --> ereal (inverse r)"
     by (auto intro!: tendsto_inverse)
   from real \<open>0 < x\<close> show ?thesis
     by (auto simp: at_ereal tendsto_compose_filtermap[symmetric] eventually_at_filter
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/FSet.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -445,12 +445,12 @@
 
 subsection \<open>Additional lemmas\<close>
 
-subsubsection \<open>@{text fsingleton}\<close>
+subsubsection \<open>\<open>fsingleton\<close>\<close>
 
 lemmas fsingletonE = fsingletonD [elim_format]
 
 
-subsubsection \<open>@{text femepty}\<close>
+subsubsection \<open>\<open>femepty\<close>\<close>
 
 lemma fempty_ffilter[simp]: "ffilter (\<lambda>_. False) A = {||}"
 by transfer auto
@@ -460,7 +460,7 @@
   by simp
 
 
-subsubsection \<open>@{text fset}\<close>
+subsubsection \<open>\<open>fset\<close>\<close>
 
 lemmas fset_simps[simp] = bot_fset.rep_eq finsert.rep_eq
 
@@ -483,7 +483,7 @@
 lemmas minus_fset[simp] = minus_fset.rep_eq
 
 
-subsubsection \<open>@{text filter_fset}\<close>
+subsubsection \<open>\<open>filter_fset\<close>\<close>
 
 lemma subset_ffilter: 
   "ffilter P A |\<subseteq>| ffilter Q A = (\<forall> x. x |\<in>| A \<longrightarrow> P x \<longrightarrow> Q x)"
@@ -499,7 +499,7 @@
   unfolding less_fset_def by (auto simp add: subset_ffilter eq_ffilter)
 
 
-subsubsection \<open>@{text finsert}\<close>
+subsubsection \<open>\<open>finsert\<close>\<close>
 
 (* FIXME, transferred doesn't work here *)
 lemma set_finsert:
@@ -511,7 +511,7 @@
   by (rule_tac x = "A |-| {|a|}" in exI, blast)
 
 
-subsubsection \<open>@{text fimage}\<close>
+subsubsection \<open>\<open>fimage\<close>\<close>
 
 lemma subset_fimage_iff: "(B |\<subseteq>| f|`|A) = (\<exists> AA. AA |\<subseteq>| A \<and> B = f|`|AA)"
 by transfer (metis mem_Collect_eq rev_finite_subset subset_image_iff)
@@ -548,7 +548,7 @@
 end
 
 
-subsubsection \<open>@{text fcard}\<close>
+subsubsection \<open>\<open>fcard\<close>\<close>
 
 (* FIXME: improve transferred to handle bounded meta quantification *)
 
@@ -631,7 +631,7 @@
 by transfer (rule card_psubset)
 
 
-subsubsection \<open>@{text ffold}\<close>
+subsubsection \<open>\<open>ffold\<close>\<close>
 
 (* FIXME: improve transferred to handle bounded meta quantification *)
 
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/FinFun.thy
--- a/src/HOL/Library/FinFun.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/FinFun.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -17,7 +17,7 @@
 \<close>
 
 
-subsection \<open>The @{text "map_default"} operation\<close>
+subsection \<open>The \<open>map_default\<close> operation\<close>
 
 definition map_default :: "'b \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
 where "map_default b f a \<equiv> case f a of None \<Rightarrow> b | Some b' \<Rightarrow> b'"
@@ -307,7 +307,7 @@
 
 quickcheck_generator finfun constructors: finfun_update_code, "finfun_const :: 'b \<Rightarrow> 'a \<Rightarrow>f 'b"
 
-subsection \<open>@{text "finfun_update"} as instance of @{text "comp_fun_commute"}\<close>
+subsection \<open>\<open>finfun_update\<close> as instance of \<open>comp_fun_commute\<close>\<close>
 
 interpretation finfun_update: comp_fun_commute "\<lambda>a f. f(a :: 'a $:= b')"
   including finfun
@@ -1525,7 +1525,7 @@
 instance by intro_classes (simp add: card_UNIV_finfun_def card_UNIV Let_def card_UNIV_finfun)
 end
 
-text \<open>Deactivate syntax again. Import theory @{text FinFun_Syntax} to reactivate it again\<close>
+text \<open>Deactivate syntax again. Import theory \<open>FinFun_Syntax\<close> to reactivate it again\<close>
 
 no_type_notation
   finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -1323,7 +1323,7 @@
 
 subsubsection \<open>Rule 3\<close>
 
-text \<open>Rule 3 is trivial and is given by @{text fps_times_def}.\<close>
+text \<open>Rule 3 is trivial and is given by \<open>fps_times_def\<close>.\<close>
 
 
 subsubsection \<open>Rule 5 --- summation and "division" by (1 - X)\<close>
@@ -3774,7 +3774,7 @@
         unfolding eventually_nhds
         apply clarsimp
         apply (rule FalseE)
-        apply auto -- \<open>slow\<close>
+        apply auto \<comment> \<open>slow\<close>
         done
       then obtain i where "inverse (2 ^ i) < e"
         by (auto simp: eventually_sequentially)
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/FuncSet.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -226,7 +226,7 @@
 
 subsection \<open>Bijections Between Sets\<close>
 
-text \<open>The definition of @{const bij_betw} is in @{text "Fun.thy"}, but most of
+text \<open>The definition of @{const bij_betw} is in \<open>Fun.thy\<close>, but most of
 the theorems belong here, or need at least @{term Hilbert_Choice}.\<close>
 
 lemma bij_betwI:
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Function_Growth.thy
--- a/src/HOL/Library/Function_Growth.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Function_Growth.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -12,39 +12,39 @@
 text \<open>
   When comparing growth of functions in computer science, it is common to adhere
   on Landau Symbols (``O-Notation'').  However these come at the cost of notational
-  oddities, particularly writing @{text "f = O(g)"} for @{text "f \<in> O(g)"} etc.
+  oddities, particularly writing \<open>f = O(g)\<close> for \<open>f \<in> O(g)\<close> etc.
   
   Here we suggest a different way, following Hardy (G.~H.~Hardy and J.~E.~Littlewood,
   Some problems of Diophantine approximation, Acta Mathematica 37 (1914), p.~225).
-  We establish a quasi order relation @{text "\<lesssim>"} on functions such that
-  @{text "f \<lesssim> g \<longleftrightarrow> f \<in> O(g)"}.  From a didactic point of view, this does not only
+  We establish a quasi order relation \<open>\<lesssim>\<close> on functions such that
+  \<open>f \<lesssim> g \<longleftrightarrow> f \<in> O(g)\<close>.  From a didactic point of view, this does not only
   avoid the notational oddities mentioned above but also emphasizes the key insight
   of a growth hierarchy of functions:
-  @{text "(\<lambda>n. 0) \<lesssim> (\<lambda>n. k) \<lesssim> Discrete.log \<lesssim> Discrete.sqrt \<lesssim> id \<lesssim> \<dots>"}.
+  \<open>(\<lambda>n. 0) \<lesssim> (\<lambda>n. k) \<lesssim> Discrete.log \<lesssim> Discrete.sqrt \<lesssim> id \<lesssim> \<dots>\<close>.
 \<close>
 
 subsection \<open>Model\<close>
 
 text \<open>
-  Our growth functions are of type @{text "\<nat> \<Rightarrow> \<nat>"}.  This is different
-  to the usual conventions for Landau symbols for which @{text "\<real> \<Rightarrow> \<real>"}
-  would be appropriate, but we argue that @{text "\<real> \<Rightarrow> \<real>"} is more
+  Our growth functions are of type \<open>\<nat> \<Rightarrow> \<nat>\<close>.  This is different
+  to the usual conventions for Landau symbols for which \<open>\<real> \<Rightarrow> \<real>\<close>
+  would be appropriate, but we argue that \<open>\<real> \<Rightarrow> \<real>\<close> is more
   appropriate for analysis, whereas our setting is discrete.
 
-  Note that we also restrict the additional coefficients to @{text \<nat>}, something
+  Note that we also restrict the additional coefficients to \<open>\<nat>\<close>, something
   we discuss at the particular definitions.
 \<close>
 
-subsection \<open>The @{text "\<lesssim>"} relation\<close>
+subsection \<open>The \<open>\<lesssim>\<close> relation\<close>
 
 definition less_eq_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<lesssim>" 50)
 where
   "f \<lesssim> g \<longleftrightarrow> (\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m)"
 
 text \<open>
-  This yields @{text "f \<lesssim> g \<longleftrightarrow> f \<in> O(g)"}.  Note that @{text c} is restricted to
-  @{text \<nat>}.  This does not pose any problems since if @{text "f \<in> O(g)"} holds for
-  a @{text "c \<in> \<real>"}, it also holds for @{text "\<lceil>c\<rceil> \<in> \<nat>"} by transitivity.
+  This yields \<open>f \<lesssim> g \<longleftrightarrow> f \<in> O(g)\<close>.  Note that \<open>c\<close> is restricted to
+  \<open>\<nat>\<close>.  This does not pose any problems since if \<open>f \<in> O(g)\<close> holds for
+  a \<open>c \<in> \<real>\<close>, it also holds for \<open>\<lceil>c\<rceil> \<in> \<nat>\<close> by transitivity.
 \<close>
 
 lemma less_eq_funI [intro?]:
@@ -68,7 +68,7 @@
   using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast
 
 
-subsection \<open>The @{text "\<approx>"} relation, the equivalence relation induced by @{text "\<lesssim>"}\<close>
+subsection \<open>The \<open>\<approx>\<close> relation, the equivalence relation induced by \<open>\<lesssim>\<close>\<close>
 
 definition equiv_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<cong>" 50)
 where
@@ -76,8 +76,8 @@
     (\<exists>c\<^sub>1>0. \<exists>c\<^sub>2>0. \<exists>n. \<forall>m>n. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m)"
 
 text \<open>
-  This yields @{text "f \<cong> g \<longleftrightarrow> f \<in> \<Theta>(g)"}.  Concerning @{text "c\<^sub>1"} and @{text "c\<^sub>2"}
-  restricted to @{typ nat}, see note above on @{text "(\<lesssim>)"}.
+  This yields \<open>f \<cong> g \<longleftrightarrow> f \<in> \<Theta>(g)\<close>.  Concerning \<open>c\<^sub>1\<close> and \<open>c\<^sub>2\<close>
+  restricted to @{typ nat}, see note above on \<open>(\<lesssim>)\<close>.
 \<close>
 
 lemma equiv_funI [intro?]:
@@ -105,7 +105,7 @@
   using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast
 
 
-subsection \<open>The @{text "\<prec>"} relation, the strict part of @{text "\<lesssim>"}\<close>
+subsection \<open>The \<open>\<prec>\<close> relation, the strict part of \<open>\<lesssim>\<close>\<close>
 
 definition less_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<prec>" 50)
 where
@@ -147,18 +147,18 @@
   using assms unfolding less_fun_def linorder_not_less [symmetric] by blast
 
 text \<open>
-  I did not find a proof for @{text "f \<prec> g \<longleftrightarrow> f \<in> o(g)"}.  Maybe this only
-  holds if @{text f} and/or @{text g} are of a certain class of functions.
-  However @{text "f \<in> o(g) \<longrightarrow> f \<prec> g"} is provable, and this yields a
+  I did not find a proof for \<open>f \<prec> g \<longleftrightarrow> f \<in> o(g)\<close>.  Maybe this only
+  holds if \<open>f\<close> and/or \<open>g\<close> are of a certain class of functions.
+  However \<open>f \<in> o(g) \<longrightarrow> f \<prec> g\<close> is provable, and this yields a
   handy introduction rule.
 
-  Note that D. Knuth ignores @{text o} altogether.  So what \dots
+  Note that D. Knuth ignores \<open>o\<close> altogether.  So what \dots
 
-  Something still has to be said about the coefficient @{text c} in
-  the definition of @{text "(\<prec>)"}.  In the typical definition of @{text o},
-  it occurs on the \emph{right} hand side of the @{text "(>)"}.  The reason
-  is that the situation is dual to the definition of @{text O}: the definition
-  works since @{text c} may become arbitrary small.  Since this is not possible
+  Something still has to be said about the coefficient \<open>c\<close> in
+  the definition of \<open>(\<prec>)\<close>.  In the typical definition of \<open>o\<close>,
+  it occurs on the \emph{right} hand side of the \<open>(>)\<close>.  The reason
+  is that the situation is dual to the definition of \<open>O\<close>: the definition
+  works since \<open>c\<close> may become arbitrary small.  Since this is not possible
   within @{term \<nat>}, we push the coefficient to the left hand side instead such
   that it become arbitrary big instead.
 \<close>
@@ -187,9 +187,9 @@
 qed
 
 
-subsection \<open>@{text "\<lesssim>"} is a preorder\<close>
+subsection \<open>\<open>\<lesssim>\<close> is a preorder\<close>
 
-text \<open>This yields all lemmas relating @{text "\<lesssim>"}, @{text "\<prec>"} and @{text "\<cong>"}.\<close>
+text \<open>This yields all lemmas relating \<open>\<lesssim>\<close>, \<open>\<prec>\<close> and \<open>\<cong>\<close>.\<close>
 
 interpretation fun_order: preorder_equiv less_eq_fun less_fun
   rewrites "preorder_equiv.equiv less_eq_fun = equiv_fun"
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -149,7 +149,7 @@
     unfolding linorder_not_le[symmetric] by blast
 qed
 
-text \<open>Hence we can always reduce modulus of @{text "1 + b z^n"} if nonzero\<close>
+text \<open>Hence we can always reduce modulus of \<open>1 + b z^n\<close> if nonzero\<close>
 lemma reduce_poly_simple:
   assumes b: "b \<noteq> 0"
     and n: "n \<noteq> 0"
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -13,7 +13,7 @@
 text \<open>
   Some elementary facts about infinite sets, mostly by Stephan Merz.
   Beware! Because "infinite" merely abbreviates a negation, these
-  lemmas may not work well with @{text "blast"}.
+  lemmas may not work well with \<open>blast\<close>.
 \<close>
 
 abbreviation infinite :: "'a set \<Rightarrow> bool"
@@ -96,7 +96,7 @@
 
 text \<open>
   For a set of natural numbers to be infinite, it is enough to know
-  that for any number larger than some @{text k}, there is some larger
+  that for any number larger than some \<open>k\<close>, there is some larger
   number that is an element of the set.
 \<close>
 
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Liminf_Limsup.thy
--- a/src/HOL/Library/Liminf_Limsup.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Liminf_Limsup.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -30,7 +30,7 @@
   shows "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
   by (rule antisym) (auto intro!: INF_greatest INF_lower2)
 
-subsubsection \<open>@{text Liminf} and @{text Limsup}\<close>
+subsubsection \<open>\<open>Liminf\<close> and \<open>Limsup\<close>\<close>
 
 definition Liminf :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
   "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)"
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/ListVector.thy
--- a/src/HOL/Library/ListVector.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/ListVector.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -18,7 +18,7 @@
 lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs"
 by (induct xs) simp_all
 
-subsection \<open>@{text"+"} and @{text"-"}\<close>
+subsection \<open>\<open>+\<close> and \<open>-\<close>\<close>
 
 fun zipwith0 :: "('a::zero \<Rightarrow> 'b::zero \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
 where
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Lub_Glb.thy
--- a/src/HOL/Library/Lub_Glb.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Lub_Glb.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -17,7 +17,7 @@
   where "x <=* S = (ALL y: S. x \<le> y)"
 
 
-subsection \<open>Rules for the Relations @{text "*<="} and @{text "<=*"}\<close>
+subsection \<open>Rules for the Relations \<open>*<=\<close> and \<open><=*\<close>\<close>
 
 lemma setleI: "ALL y: S. y \<le> x \<Longrightarrow> S *<= x"
   by (simp add: setle_def)
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Mapping.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -10,7 +10,7 @@
 
 subsection \<open>Parametricity transfer rules\<close>
 
-lemma map_of_foldr: -- \<open>FIXME move\<close>
+lemma map_of_foldr: \<comment> \<open>FIXME move\<close>
   "map_of xs = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) xs Map.empty"
   using map_add_map_of_foldr [of Map.empty] by auto
 
@@ -107,7 +107,7 @@
   is "\<lambda>m k. m k" parametric lookup_parametric .
 
 declare [[code drop: Mapping.lookup]]
-setup \<open>Code.add_default_eqn @{thm Mapping.lookup.abs_eq}\<close> -- \<open>FIXME lifting\<close>
+setup \<open>Code.add_default_eqn @{thm Mapping.lookup.abs_eq}\<close> \<comment> \<open>FIXME lifting\<close>
 
 lift_definition update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping"
   is "\<lambda>k v m. m(k \<mapsto> v)" parametric update_parametric .
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Multiset.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -809,12 +809,11 @@
 text \<open>
   A note on code generation: When defining some function containing a
   subterm @{term "fold_mset F"}, code generation is not automatic. When
-  interpreting locale @{text left_commutative} with @{text F}, the
+  interpreting locale \<open>left_commutative\<close> with \<open>F\<close>, the
   would be code thms for @{const fold_mset} become thms like
-  @{term "fold_mset F z {#} = z"} where @{text F} is not a pattern but
+  @{term "fold_mset F z {#} = z"} where \<open>F\<close> is not a pattern but
   contains defined symbols, i.e.\ is not a code thm. Hence a separate
-  constant with its own code thms needs to be introduced for @{text
-  F}. See the image operator below.
+  constant with its own code thms needs to be introduced for \<open>F\<close>. See the image operator below.
 \<close>
 
 
@@ -1083,7 +1082,7 @@
   qed
   then show "PROP ?P" "PROP ?Q" "PROP ?R"
   by (auto elim!: Set.set_insert)
-qed -- \<open>TODO: maybe define @{const mset_set} also in terms of @{const Abs_multiset}\<close>
+qed \<comment> \<open>TODO: maybe define @{const mset_set} also in terms of @{const Abs_multiset}\<close>
 
 lemma elem_mset_set[simp, intro]: "finite A \<Longrightarrow> x \<in># mset_set A \<longleftrightarrow> x \<in> A"
   by (induct A rule: finite_induct) simp_all
@@ -1349,7 +1348,7 @@
 
 text \<open>
   This lemma shows which properties suffice to show that a function
-  @{text "f"} with @{text "f xs = ys"} behaves like sort.
+  \<open>f\<close> with \<open>f xs = ys\<close> behaves like sort.
 \<close>
 
 lemma properties_for_sort_key:
@@ -2106,7 +2105,7 @@
 
 declare sorted_list_of_multiset_mset [code]
 
-lemma [code]: -- \<open>not very efficient, but representation-ignorant!\<close>
+lemma [code]: \<comment> \<open>not very efficient, but representation-ignorant!\<close>
   "mset_set A = mset (sorted_list_of_set A)"
   apply (cases "finite A")
   apply simp_all
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -182,7 +182,7 @@
 subsection \<open>Ring class instances\<close>
 
 text \<open>
-  Unfortunately @{text ring_1} instance is not possible for
+  Unfortunately \<open>ring_1\<close> instance is not possible for
   @{typ num1}, since 0 and 1 are not distinct.
 \<close>
 
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Old_Datatype.thy
--- a/src/HOL/Library/Old_Datatype.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Old_Datatype.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -21,7 +21,7 @@
   morphisms Rep_Node Abs_Node
   unfolding Node_def by auto
 
-text\<open>Datatypes will be represented by sets of type @{text node}\<close>
+text\<open>Datatypes will be represented by sets of type \<open>node\<close>\<close>
 
 type_synonym 'a item        = "('a, unit) node set"
 type_synonym ('a, 'b) dtree = "('a, 'b) node set"
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Old_SMT.thy
--- a/src/HOL/Library/Old_SMT.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Old_SMT.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -51,7 +51,7 @@
 definition weight :: "int \<Rightarrow> bool \<Rightarrow> bool" where "weight _ P = P"
 
 text \<open>
-Weights must be non-negative.  The value @{text 0} is equivalent to providing
+Weights must be non-negative.  The value \<open>0\<close> is equivalent to providing
 no weight at all.
 
 Weights should only be used at quantifiers and only inside triggers (if the
@@ -150,7 +150,7 @@
 
 text \<open>
 The current configuration can be printed by the command
-@{text old_smt_status}, which shows the values of most options.
+\<open>old_smt_status\<close>, which shows the values of most options.
 \<close>
 
 
@@ -158,14 +158,14 @@
 subsection \<open>General configuration options\<close>
 
 text \<open>
-The option @{text old_smt_solver} can be used to change the target SMT
-solver.  The possible values can be obtained from the @{text old_smt_status}
+The option \<open>old_smt_solver\<close> can be used to change the target SMT
+solver.  The possible values can be obtained from the \<open>old_smt_status\<close>
 command.
 
 Due to licensing restrictions, Yices and Z3 are not installed/enabled
 by default.  Z3 is free for non-commercial applications and can be enabled
-by setting the @{text OLD_Z3_NON_COMMERCIAL} environment variable to
-@{text yes}.
+by setting the \<open>OLD_Z3_NON_COMMERCIAL\<close> environment variable to
+\<open>yes\<close>.
 \<close>
 
 declare [[ old_smt_solver = z3 ]]
@@ -242,7 +242,7 @@
 subsection \<open>Certificates\<close>
 
 text \<open>
-By setting the option @{text old_smt_certificates} to the name of a file,
+By setting the option \<open>old_smt_certificates\<close> to the name of a file,
 all following applications of an SMT solver a cached in that file.
 Any further application of the same SMT solver (using the very same
 configuration) re-uses the cached certificate instead of invoking the
@@ -250,7 +250,7 @@
 
 The filename should be given as an explicit path.  It is good
 practice to use the name of the current theory (with ending
-@{text ".certs"} instead of @{text ".thy"}) as the certificates file.
+\<open>.certs\<close> instead of \<open>.thy\<close>) as the certificates file.
 Certificate files should be used at most once in a certain theory context,
 to avoid race conditions with other concurrent accesses.
 \<close>
@@ -258,11 +258,11 @@
 declare [[ old_smt_certificates = "" ]]
 
 text \<open>
-The option @{text old_smt_read_only_certificates} controls whether only
+The option \<open>old_smt_read_only_certificates\<close> controls whether only
 stored certificates are should be used or invocation of an SMT solver
-is allowed.  When set to @{text true}, no SMT solver will ever be
+is allowed.  When set to \<open>true\<close>, no SMT solver will ever be
 invoked and only the existing certificates found in the configured
-cache are used;  when set to @{text false} and there is no cached
+cache are used;  when set to \<open>false\<close> and there is no cached
 certificate for some proposition, then the configured SMT solver is
 invoked.
 \<close>
@@ -275,7 +275,7 @@
 
 text \<open>
 The SMT method, when applied, traces important information.  To
-make it entirely silent, set the following option to @{text false}.
+make it entirely silent, set the following option to \<open>false\<close>.
 \<close>
 
 declare [[ old_smt_verbose = true ]]
@@ -283,7 +283,7 @@
 text \<open>
 For tracing the generated problem file given to the SMT solver as
 well as the returned result of the solver, the option
-@{text old_smt_trace} should be set to @{text true}.
+\<open>old_smt_trace\<close> should be set to \<open>true\<close>.
 \<close>
 
 declare [[ old_smt_trace = false ]]
@@ -292,7 +292,7 @@
 From the set of assumptions given to the SMT solver, those assumptions
 used in the proof are traced when the following option is set to
 @{term true}.  This only works for Z3 when it runs in non-oracle mode
-(see options @{text old_smt_solver} and @{text old_smt_oracle} above).
+(see options \<open>old_smt_solver\<close> and \<open>old_smt_oracle\<close> above).
 \<close>
 
 declare [[ old_smt_trace_used_facts = false ]]
@@ -304,9 +304,9 @@
 text \<open>
 Several prof rules of Z3 are not very well documented.  There are two
 lemma groups which can turn failing Z3 proof reconstruction attempts
-into succeeding ones: the facts in @{text z3_rule} are tried prior to
+into succeeding ones: the facts in \<open>z3_rule\<close> are tried prior to
 any implemented reconstruction procedure for all uncertain Z3 proof
-rules;  the facts in @{text z3_simp} are only fed to invocations of
+rules;  the facts in \<open>z3_simp\<close> are only fed to invocations of
 the simplifier when reconstructing theory-specific proof steps.
 \<close>
 
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Omega_Words_Fun.thy
--- a/src/HOL/Library/Omega_Words_Fun.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Omega_Words_Fun.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -529,20 +529,20 @@
 proof -
   have "\<exists>k. range (suffix k x) \<subseteq> limit x"
   proof -
-    -- "The set of letters that are not in the limit is certainly finite."
+    \<comment> "The set of letters that are not in the limit is certainly finite."
     from fin have "finite (range x - limit x)"
       by simp
-    -- "Moreover, any such letter occurs only finitely often"
+    \<comment> "Moreover, any such letter occurs only finitely often"
     moreover
     have "\<forall>a \<in> range x - limit x. finite (x -` {a})"
       by (auto simp add: limit_vimage)
-    -- "Thus, there are only finitely many occurrences of such letters."
+    \<comment> "Thus, there are only finitely many occurrences of such letters."
     ultimately have "finite (UN a : range x - limit x. x -` {a})"
       by (blast intro: finite_UN_I)
-    -- "Therefore these occurrences are within some initial interval."
+    \<comment> "Therefore these occurrences are within some initial interval."
     then obtain k where "(UN a : range x - limit x. x -` {a}) \<subseteq> {..<k}"
       by (blast dest: finite_nat_bounded)
-    -- "This is just the bound we are looking for."
+    \<comment> "This is just the bound we are looking for."
     hence "\<forall>m. k \<le> m \<longrightarrow> x m \<in> limit x"
       by (auto simp add: limit_vimage)
     hence "range (suffix k x) \<subseteq> limit x"
@@ -624,11 +624,11 @@
     fix a assume a: "a \<in> set w"
     then obtain k where k: "k < length w \<and> w!k = a"
       by (auto simp add: set_conv_nth)
-    -- "the following bound is terrible, but it simplifies the proof"
+    \<comment> "the following bound is terrible, but it simplifies the proof"
     from nempty k have "\<forall>m. w\<^sup>\<omega> ((Suc m)*(length w) + k) = a"
       by (simp add: mod_add_left_eq)
     moreover
-    -- "why is the following so hard to prove??"
+    \<comment> "why is the following so hard to prove??"
     have "\<forall>m. m < (Suc m)*(length w) + k"
     proof
       fix m
@@ -661,7 +661,7 @@
 text \<open>
   The converse relation is not true in general: $f(a)$ can be in the
   limit of $f \circ w$ even though $a$ is not in the limit of $w$.
-  However, @{text limit} commutes with renaming if the function is
+  However, \<open>limit\<close> commutes with renaming if the function is
   injective. More generally, if $f(a)$ is the image of only finitely
   many elements, some of these must be in the limit of $w$.
 \<close>
@@ -672,21 +672,21 @@
   shows "\<exists>a \<in> (f -` {x}). a \<in> limit w"
 proof (rule ccontr)
   assume contra: "\<not> ?thesis"
-  -- "hence, every element in the pre-image occurs only finitely often"
+  \<comment> "hence, every element in the pre-image occurs only finitely often"
   then have "\<forall>a \<in> (f -` {x}). finite {n. w n = a}"
     by (simp add: limit_def Inf_many_def)
-  -- "so there are only finitely many occurrences of any such element"
+  \<comment> "so there are only finitely many occurrences of any such element"
   with fin have "finite (\<Union> a \<in> (f -` {x}). {n. w n = a})"
     by auto
-  -- \<open>these are precisely those positions where $x$ occurs in $f \circ w$\<close>
+  \<comment> \<open>these are precisely those positions where $x$ occurs in $f \circ w$\<close>
   moreover
   have "(\<Union> a \<in> (f -` {x}). {n. w n = a}) = {n. f(w n) = x}"
     by auto
   ultimately
-  -- "so $x$ can occur only finitely often in the translated word"
+  \<comment> "so $x$ can occur only finitely often in the translated word"
   have "finite {n. f(w n) = x}"
     by simp
-  -- \<open>\ldots\ which yields a contradiction\<close>
+  \<comment> \<open>\ldots\ which yields a contradiction\<close>
   with x show "False"
     by (simp add: limit_def Inf_many_def)
 qed
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Order_Continuity.thy
--- a/src/HOL/Library/Order_Continuity.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Order_Continuity.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -29,8 +29,8 @@
   done
 
 text \<open>
-  The name @{text continuous} is already taken in @{text "Complex_Main"}, so we use
-  @{text "sup_continuous"} and @{text "inf_continuous"}. These names appear sometimes in literature
+  The name \<open>continuous\<close> is already taken in \<open>Complex_Main\<close>, so we use
+  \<open>sup_continuous\<close> and \<open>inf_continuous\<close>. These names appear sometimes in literature
   and have the advantage that these names are duals.
 \<close>
 
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Permutation.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -116,7 +116,7 @@
   apply (safe intro!: perm_append2)
   apply (rule append_perm_imp_perm)
   apply (rule perm_append_swap [THEN perm.trans])
-    -- \<open>the previous step helps this @{text blast} call succeed quickly\<close>
+    \<comment> \<open>the previous step helps this \<open>blast\<close> call succeed quickly\<close>
   apply (blast intro: perm_append_swap)
   done
 
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Polynomial.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -50,7 +50,7 @@
   "tl (x ## xs) = xs"
   by (simp add: cCons_def)
 
-subsection \<open>Definition of type @{text poly}\<close>
+subsection \<open>Definition of type \<open>poly\<close>\<close>
 
 typedef (overloaded) 'a poly = "{f :: nat \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n. f n = 0}"
   morphisms coeff Abs_poly by (auto intro!: ALL_MOST)
@@ -440,7 +440,7 @@
 
 definition poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a"
 where
-  "poly p = fold_coeffs (\<lambda>a f x. a + x * f x) p (\<lambda>x. 0)" -- \<open>The Horner Schema\<close>
+  "poly p = fold_coeffs (\<lambda>a f x. a + x * f x) p (\<lambda>x. 0)" \<comment> \<open>The Horner Schema\<close>
 
 lemma poly_0 [simp]:
   "poly 0 x = 0"
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -177,7 +177,7 @@
 
 section \<open>Alternative list definitions\<close>
 
-subsection \<open>Alternative rules for @{text length}\<close>
+subsection \<open>Alternative rules for \<open>length\<close>\<close>
 
 definition size_list' :: "'a list => nat"
 where "size_list' = size"
@@ -191,7 +191,7 @@
 declare size_list'_def[symmetric, code_pred_inline]
 
 
-subsection \<open>Alternative rules for @{text list_all2}\<close>
+subsection \<open>Alternative rules for \<open>list_all2\<close>\<close>
 
 lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"
 by auto
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Quotient_Type.thy
--- a/src/HOL/Library/Quotient_Type.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Quotient_Type.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -14,8 +14,8 @@
 
 subsection \<open>Equivalence relations and quotient types\<close>
 
-text \<open>Type class @{text equiv} models equivalence relations
-  @{text "\<sim> :: 'a \<Rightarrow> 'a \<Rightarrow> bool"}.\<close>
+text \<open>Type class \<open>equiv\<close> models equivalence relations
+  \<open>\<sim> :: 'a \<Rightarrow> 'a \<Rightarrow> bool\<close>.\<close>
 
 class eqv =
   fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infixl "\<sim>" 50)
@@ -57,7 +57,7 @@
 
 end
 
-text \<open>The quotient type @{text "'a quot"} consists of all \emph{equivalence
+text \<open>The quotient type \<open>'a quot\<close> consists of all \emph{equivalence
   classes} over elements of the base type @{typ 'a}.\<close>
 
 definition (in eqv) "quot = {{x. a \<sim> x} | a. True}"
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/RBT_Impl.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -10,7 +10,7 @@
 begin
 
 text \<open>
-  For applications, you should use theory @{text RBT} which defines
+  For applications, you should use theory \<open>RBT\<close> which defines
   an abstract type of red-black tree obeying the invariant.
 \<close>
 
@@ -305,7 +305,7 @@
   "inv1 Empty = True"
 | "inv1 (Branch c lt k v rt) \<longleftrightarrow> inv1 lt \<and> inv1 rt \<and> (c = B \<or> color_of lt = B \<and> color_of rt = B)"
 
-primrec inv1l :: "('a, 'b) rbt \<Rightarrow> bool" -- \<open>Weaker version\<close>
+primrec inv1l :: "('a, 'b) rbt \<Rightarrow> bool" \<comment> \<open>Weaker version\<close>
 where
   "inv1l Empty = True"
 | "inv1l (Branch c l k v r) = (inv1 l \<and> inv1 r)"
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/RBT_Mapping.thy
--- a/src/HOL/Library/RBT_Mapping.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/RBT_Mapping.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -100,11 +100,11 @@
 text \<open>
   The type @{typ "('k, 'v) RBT_Impl.rbt"} denotes red-black trees with
   keys of type @{typ "'k"} and values of type @{typ "'v"}. To function
-  properly, the key type musorted belong to the @{text "linorder"}
+  properly, the key type musorted belong to the \<open>linorder\<close>
   class.
 
   A value @{term t} of this type is a valid red-black tree if it
-  satisfies the invariant @{text "is_rbt t"}.  The abstract type @{typ
+  satisfies the invariant \<open>is_rbt t\<close>.  The abstract type @{typ
   "('k, 'v) rbt"} always obeys this invariant, and for this reason you
   should only use this in our application.  Going back to @{typ "('k,
   'v) RBT_Impl.rbt"} may be necessary in proofs if not yet proven
@@ -155,25 +155,25 @@
 
 text \<open>
   \noindent
-  @{thm Empty_is_rbt}\hfill(@{text "Empty_is_rbt"})
+  @{thm Empty_is_rbt}\hfill(\<open>Empty_is_rbt\<close>)
 
   \noindent
-  @{thm rbt_insert_is_rbt}\hfill(@{text "rbt_insert_is_rbt"})
+  @{thm rbt_insert_is_rbt}\hfill(\<open>rbt_insert_is_rbt\<close>)
 
   \noindent
-  @{thm rbt_delete_is_rbt}\hfill(@{text "delete_is_rbt"})
+  @{thm rbt_delete_is_rbt}\hfill(\<open>delete_is_rbt\<close>)
 
   \noindent
-  @{thm rbt_bulkload_is_rbt}\hfill(@{text "bulkload_is_rbt"})
+  @{thm rbt_bulkload_is_rbt}\hfill(\<open>bulkload_is_rbt\<close>)
 
   \noindent
-  @{thm rbt_map_entry_is_rbt}\hfill(@{text "map_entry_is_rbt"})
+  @{thm rbt_map_entry_is_rbt}\hfill(\<open>map_entry_is_rbt\<close>)
 
   \noindent
-  @{thm map_is_rbt}\hfill(@{text "map_is_rbt"})
+  @{thm map_is_rbt}\hfill(\<open>map_is_rbt\<close>)
 
   \noindent
-  @{thm rbt_union_is_rbt}\hfill(@{text "union_is_rbt"})
+  @{thm rbt_union_is_rbt}\hfill(\<open>union_is_rbt\<close>)
 \<close>
 
 
@@ -181,27 +181,27 @@
 
 text \<open>
   \noindent
-  \underline{@{text "lookup_empty"}}
+  \underline{\<open>lookup_empty\<close>}
   @{thm [display] lookup_empty}
   \vspace{1ex}
 
   \noindent
-  \underline{@{text "lookup_insert"}}
+  \underline{\<open>lookup_insert\<close>}
   @{thm [display] lookup_insert}
   \vspace{1ex}
 
   \noindent
-  \underline{@{text "lookup_delete"}}
+  \underline{\<open>lookup_delete\<close>}
   @{thm [display] lookup_delete}
   \vspace{1ex}
 
   \noindent
-  \underline{@{text "lookup_bulkload"}}
+  \underline{\<open>lookup_bulkload\<close>}
   @{thm [display] lookup_bulkload}
   \vspace{1ex}
 
   \noindent
-  \underline{@{text "lookup_map"}}
+  \underline{\<open>lookup_map\<close>}
   @{thm [display] lookup_map}
   \vspace{1ex}
 \<close>
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Ramsey.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -120,7 +120,7 @@
 subsubsection \<open>``Axiom'' of Dependent Choice\<close>
 
 primrec choice :: "('a => bool) => ('a * 'a) set => nat => 'a" where
-  --\<open>An integer-indexed chain of choices\<close>
+  \<comment>\<open>An integer-indexed chain of choices\<close>
     choice_0:   "choice P r 0 = (SOME x. P x)"
   | choice_Suc: "choice P r (Suc n) = (SOME y. P y & (choice P r n, y) \<in> r)"
 
@@ -157,7 +157,7 @@
 subsubsection \<open>Partitions of a Set\<close>
 
 definition part :: "nat => nat => 'a set => ('a set => nat) => bool"
-  --\<open>the function @{term f} partitions the @{term r}-subsets of the typically
+  \<comment>\<open>the function @{term f} partitions the @{term r}-subsets of the typically
        infinite set @{term Y} into @{term s} distinct categories.\<close>
 where
   "part r s Y f = (\<forall>X. X \<subseteq> Y & finite X & card X = r --> f X < s)"
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Set_Algebras.thy
--- a/src/HOL/Library/Set_Algebras.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Set_Algebras.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -11,7 +11,7 @@
 text \<open>
   This library lifts operations like addition and multiplication to
   sets.  It was designed to support asymptotic calculations. See the
-  comments at the top of theory @{text BigO}.
+  comments at the top of theory \<open>BigO\<close>.
 \<close>
 
 instantiation set :: (plus) plus
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/State_Monad.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -32,26 +32,26 @@
 
   \begin{description}
 
-    \item[transformations] with type signature @{text "\<sigma> \<Rightarrow> \<sigma>'"},
+    \item[transformations] with type signature \<open>\<sigma> \<Rightarrow> \<sigma>'\<close>,
       transforming a state.
 
-    \item[``yielding'' transformations] with type signature @{text "\<sigma>
-      \<Rightarrow> \<alpha> \<times> \<sigma>'"}, ``yielding'' a side result while transforming a
+    \item[``yielding'' transformations] with type signature \<open>\<sigma>
+      \<Rightarrow> \<alpha> \<times> \<sigma>'\<close>, ``yielding'' a side result while transforming a
       state.
 
-    \item[queries] with type signature @{text "\<sigma> \<Rightarrow> \<alpha>"}, computing a
+    \item[queries] with type signature \<open>\<sigma> \<Rightarrow> \<alpha>\<close>, computing a
       result dependent on a state.
 
   \end{description}
 
-  By convention we write @{text "\<sigma>"} for types representing states and
-  @{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"} for types
+  By convention we write \<open>\<sigma>\<close> for types representing states and
+  \<open>\<alpha>\<close>, \<open>\<beta>\<close>, \<open>\<gamma>\<close>, \<open>\<dots>\<close> for types
   representing side results.  Type changes due to transformations are
   not excluded in our scenario.
 
-  We aim to assert that values of any state type @{text "\<sigma>"} are used
+  We aim to assert that values of any state type \<open>\<sigma>\<close> are used
   in a single-threaded way: after application of a transformation on a
-  value of type @{text "\<sigma>"}, the former value should not be used
+  value of type \<open>\<sigma>\<close>, the former value should not be used
   again.  To achieve this, we use a set of monad combinators:
 \<close>
 
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Sublist_Order.thy
--- a/src/HOL/Library/Sublist_Order.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Sublist_Order.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -11,8 +11,8 @@
 
 text \<open>
   This theory defines sublist ordering on lists.
-  A list @{text ys} is a sublist of a list @{text xs},
-  iff one obtains @{text ys} by erasing some elements from @{text xs}.
+  A list \<open>ys\<close> is a sublist of a list \<open>xs\<close>,
+  iff one obtains \<open>ys\<close> by erasing some elements from \<open>xs\<close>.
 \<close>
 
 subsection \<open>Definitions and basic lemmas\<close>
diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Tree.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -146,7 +146,7 @@
   (heap l \<and> heap r \<and> (\<forall>x \<in> set_tree l \<union> set_tree r. m \<le> x))"
 
 
-subsection "Function @{text mirror}"
+subsection "Function \<open>mirror\<close>"
 
 fun mirror :: "'a tree \<Rightarrow> 'a tree" where
 "mirror \<langle>\<rangle> = Leaf" |