isabelle update_cartouches -c -t;
authorwenzelm
Thu Nov 05 10:39:49 2015 +0100 (2015-11-05)
changeset 61585a9599d3d7610
parent 61584 f06e5a5a4b46
child 61586 5197a2ecb658
isabelle update_cartouches -c -t;
src/HOL/Library/AList.thy
src/HOL/Library/BigO.thy
src/HOL/Library/Cardinality.thy
src/HOL/Library/Code_Char.thy
src/HOL/Library/Code_Target_Nat.thy
src/HOL/Library/Code_Test.thy
src/HOL/Library/ContNotDenum.thy
src/HOL/Library/Convex.thy
src/HOL/Library/Countable_Set_Type.thy
src/HOL/Library/DAList.thy
src/HOL/Library/DAList_Multiset.thy
src/HOL/Library/Debug.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/FSet.thy
src/HOL/Library/FinFun.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/FuncSet.thy
src/HOL/Library/Function_Growth.thy
src/HOL/Library/Fundamental_Theorem_Algebra.thy
src/HOL/Library/Infinite_Set.thy
src/HOL/Library/Liminf_Limsup.thy
src/HOL/Library/ListVector.thy
src/HOL/Library/Lub_Glb.thy
src/HOL/Library/Mapping.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/Library/Old_Datatype.thy
src/HOL/Library/Old_SMT.thy
src/HOL/Library/Omega_Words_Fun.thy
src/HOL/Library/Order_Continuity.thy
src/HOL/Library/Permutation.thy
src/HOL/Library/Polynomial.thy
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
src/HOL/Library/Quotient_Type.thy
src/HOL/Library/RBT_Impl.thy
src/HOL/Library/RBT_Mapping.thy
src/HOL/Library/Ramsey.thy
src/HOL/Library/Set_Algebras.thy
src/HOL/Library/State_Monad.thy
src/HOL/Library/Sublist_Order.thy
src/HOL/Library/Tree.thy
     1.1 --- a/src/HOL/Library/AList.thy	Thu Nov 05 10:35:37 2015 +0100
     1.2 +++ b/src/HOL/Library/AList.thy	Thu Nov 05 10:39:49 2015 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4    to establish the invariant, e.g. for inductive proofs.
     1.5  \<close>
     1.6  
     1.7 -subsection \<open>@{text update} and @{text updates}\<close>
     1.8 +subsection \<open>\<open>update\<close> and \<open>updates\<close>\<close>
     1.9  
    1.10  qualified primrec update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.11  where
    1.12 @@ -163,7 +163,7 @@
    1.13    by (induct xs arbitrary: ys al) (auto split: list.splits)
    1.14  
    1.15  
    1.16 -subsection \<open>@{text delete}\<close>
    1.17 +subsection \<open>\<open>delete\<close>\<close>
    1.18  
    1.19  qualified definition delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.20    where delete_eq: "delete k = filter (\<lambda>(k', _). k \<noteq> k')"
    1.21 @@ -215,7 +215,7 @@
    1.22    by (simp add: delete_eq)
    1.23  
    1.24  
    1.25 -subsection \<open>@{text update_with_aux} and @{text delete_aux}\<close>
    1.26 +subsection \<open>\<open>update_with_aux\<close> and \<open>delete_aux\<close>\<close>
    1.27  
    1.28  qualified primrec update_with_aux :: "'val \<Rightarrow> 'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.29  where
    1.30 @@ -296,7 +296,7 @@
    1.31  by(cases ts)(auto split: split_if_asm)
    1.32  
    1.33  
    1.34 -subsection \<open>@{text restrict}\<close>
    1.35 +subsection \<open>\<open>restrict\<close>\<close>
    1.36  
    1.37  qualified definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.38    where restrict_eq: "restrict A = filter (\<lambda>(k, v). k \<in> A)"
    1.39 @@ -380,7 +380,7 @@
    1.40    by (induct ps) auto
    1.41  
    1.42  
    1.43 -subsection \<open>@{text clearjunk}\<close>
    1.44 +subsection \<open>\<open>clearjunk\<close>\<close>
    1.45  
    1.46  qualified function clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.47  where
    1.48 @@ -464,7 +464,7 @@
    1.49      (simp_all add: clearjunk_delete delete_map assms)
    1.50  
    1.51  
    1.52 -subsection \<open>@{text map_ran}\<close>
    1.53 +subsection \<open>\<open>map_ran\<close>\<close>
    1.54  
    1.55  definition map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.56    where "map_ran f = map (\<lambda>(k, v). (k, f k v))"
    1.57 @@ -490,7 +490,7 @@
    1.58    by (simp add: map_ran_def split_def clearjunk_map)
    1.59  
    1.60  
    1.61 -subsection \<open>@{text merge}\<close>
    1.62 +subsection \<open>\<open>merge\<close>\<close>
    1.63  
    1.64  qualified definition merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.65    where "merge qs ps = foldr (\<lambda>(k, v). update k v) ps qs"
    1.66 @@ -558,7 +558,7 @@
    1.67    by (simp add: merge_conv')
    1.68  
    1.69  
    1.70 -subsection \<open>@{text compose}\<close>
    1.71 +subsection \<open>\<open>compose\<close>\<close>
    1.72  
    1.73  qualified function compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list"
    1.74  where
    1.75 @@ -723,7 +723,7 @@
    1.76    by (simp add: compose_conv map_comp_None_iff)
    1.77  
    1.78  
    1.79 -subsection \<open>@{text map_entry}\<close>
    1.80 +subsection \<open>\<open>map_entry\<close>\<close>
    1.81  
    1.82  qualified fun map_entry :: "'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.83  where
    1.84 @@ -745,7 +745,7 @@
    1.85    using assms by (induct xs) (auto simp add: dom_map_entry)
    1.86  
    1.87  
    1.88 -subsection \<open>@{text map_default}\<close>
    1.89 +subsection \<open>\<open>map_default\<close>\<close>
    1.90  
    1.91  fun map_default :: "'key \<Rightarrow> 'val \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.92  where
     2.1 --- a/src/HOL/Library/BigO.thy	Thu Nov 05 10:35:37 2015 +0100
     2.2 +++ b/src/HOL/Library/BigO.thy	Thu Nov 05 10:39:49 2015 +0100
     2.3 @@ -16,20 +16,20 @@
     2.4  
     2.5  The main changes in this version are as follows:
     2.6  \begin{itemize}
     2.7 -\item We have eliminated the @{text O} operator on sets. (Most uses of this seem
     2.8 +\item We have eliminated the \<open>O\<close> operator on sets. (Most uses of this seem
     2.9    to be inessential.)
    2.10 -\item We no longer use @{text "+"} as output syntax for @{text "+o"}
    2.11 -\item Lemmas involving @{text "sumr"} have been replaced by more general lemmas
    2.12 -  involving `@{text "setsum"}.
    2.13 +\item We no longer use \<open>+\<close> as output syntax for \<open>+o\<close>
    2.14 +\item Lemmas involving \<open>sumr\<close> have been replaced by more general lemmas
    2.15 +  involving `\<open>setsum\<close>.
    2.16  \item The library has been expanded, with e.g.~support for expressions of
    2.17 -  the form @{text "f < g + O(h)"}.
    2.18 +  the form \<open>f < g + O(h)\<close>.
    2.19  \end{itemize}
    2.20  
    2.21  Note also since the Big O library includes rules that demonstrate set
    2.22  inclusion, to use the automated reasoners effectively with the library
    2.23 -one should redeclare the theorem @{text "subsetI"} as an intro rule,
    2.24 -rather than as an @{text "intro!"} rule, for example, using
    2.25 -\isa{\isakeyword{declare}}~@{text "subsetI [del, intro]"}.
    2.26 +one should redeclare the theorem \<open>subsetI\<close> as an intro rule,
    2.27 +rather than as an \<open>intro!\<close> rule, for example, using
    2.28 +\isa{\isakeyword{declare}}~\<open>subsetI [del, intro]\<close>.
    2.29  \<close>
    2.30  
    2.31  subsection \<open>Definitions\<close>
     3.1 --- a/src/HOL/Library/Cardinality.thy	Thu Nov 05 10:35:37 2015 +0100
     3.2 +++ b/src/HOL/Library/Cardinality.thy	Thu Nov 05 10:39:49 2015 +0100
     3.3 @@ -211,7 +211,7 @@
     3.4    fixes card_UNIV :: "'a card_UNIV"
     3.5    assumes card_UNIV: "card_UNIV = Phantom('a) CARD('a)"
     3.6  
     3.7 -subsection \<open>Instantiations for @{text "card_UNIV"}\<close>
     3.8 +subsection \<open>Instantiations for \<open>card_UNIV\<close>\<close>
     3.9  
    3.10  instantiation nat :: card_UNIV begin
    3.11  definition "finite_UNIV = Phantom(nat) False"
    3.12 @@ -534,7 +534,7 @@
    3.13       (\<lambda>_. List.coset xs \<subseteq> set ys))"
    3.14  by simp
    3.15  
    3.16 -notepad begin -- "test code setup"
    3.17 +notepad begin \<comment> "test code setup"
    3.18  have "List.coset [True] = set [False] \<and> 
    3.19        List.coset [] \<subseteq> List.set [True, False] \<and> 
    3.20        finite (List.coset [True])"
     4.1 --- a/src/HOL/Library/Code_Char.thy	Thu Nov 05 10:35:37 2015 +0100
     4.2 +++ b/src/HOL/Library/Code_Char.thy	Thu Nov 05 10:39:49 2015 +0100
     4.3 @@ -107,7 +107,7 @@
     4.4  |  constant "Orderings.less_eq :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
     4.5      (SML) "!((_ : string) <= _)"
     4.6      and (OCaml) "!((_ : string) <= _)"
     4.7 -    -- \<open>Order operations for @{typ String.literal} work in Haskell only 
     4.8 +    \<comment> \<open>Order operations for @{typ String.literal} work in Haskell only 
     4.9            if no type class instance needs to be generated, because String = [Char] in Haskell
    4.10            and @{typ "char list"} need not have the same order as @{typ String.literal}.\<close>
    4.11      and (Haskell) infix 4 "<="
     5.1 --- a/src/HOL/Library/Code_Target_Nat.thy	Thu Nov 05 10:35:37 2015 +0100
     5.2 +++ b/src/HOL/Library/Code_Target_Nat.thy	Thu Nov 05 10:39:49 2015 +0100
     5.3 @@ -135,7 +135,7 @@
     5.4    including integer.lifting by transfer auto
     5.5  
     5.6  lemma term_of_nat_code [code]:
     5.7 -  -- \<open>Use @{term Code_Numeral.nat_of_integer} in term reconstruction
     5.8 +  \<comment> \<open>Use @{term Code_Numeral.nat_of_integer} in term reconstruction
     5.9          instead of @{term Code_Target_Nat.Nat} such that reconstructed
    5.10          terms can be fed back to the code generator\<close>
    5.11    "term_of_class.term_of n =
     6.1 --- a/src/HOL/Library/Code_Test.thy	Thu Nov 05 10:35:37 2015 +0100
     6.2 +++ b/src/HOL/Library/Code_Test.thy	Thu Nov 05 10:39:49 2015 +0100
     6.3 @@ -131,7 +131,7 @@
     6.4    "xml_of_term (Code_Evaluation.Const x ty) = [xml.tagged (STR ''0'') (Some x) (xml_of_typ ty)]"
     6.5    "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)]]"
     6.6    "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)]]"
     6.7 -  -- \<open>
     6.8 +  \<comment> \<open>
     6.9      FIXME: @{const Code_Evaluation.Free} is used only in @{theory Quickcheck_Narrowing} to represent
    6.10      uninstantiated parameters in constructors. Here, we always translate them to @{ML Free} variables.
    6.11  \<close>
     7.1 --- a/src/HOL/Library/ContNotDenum.thy	Thu Nov 05 10:35:37 2015 +0100
     7.2 +++ b/src/HOL/Library/ContNotDenum.thy	Thu Nov 05 10:39:49 2015 +0100
     7.3 @@ -15,8 +15,8 @@
     7.4  uncountable. It is formalised in the Isabelle/Isar theorem proving
     7.5  system.
     7.6  
     7.7 -{\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other
     7.8 -words, there does not exist a function @{text "f: \<nat> \<Rightarrow> \<real>"} such that f is
     7.9 +{\em Theorem:} The Continuum \<open>\<real>\<close> is not denumerable. In other
    7.10 +words, there does not exist a function \<open>f: \<nat> \<Rightarrow> \<real>\<close> such that f is
    7.11  surjective.
    7.12  
    7.13  {\em Outline:} An elegant informal proof of this result uses Cantor's
    7.14 @@ -26,8 +26,7 @@
    7.15  completeness of the Real numbers and is the foundation for our
    7.16  argument. Informally it states that an intersection of countable
    7.17  closed intervals (where each successive interval is a subset of the
    7.18 -last) is non-empty. We then assume a surjective function @{text
    7.19 -"f: \<nat> \<Rightarrow> \<real>"} exists and find a real x such that x is not in the range of f
    7.20 +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
    7.21  by generating a sequence of closed intervals then using the NIP.\<close>
    7.22  
    7.23  theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)"
     8.1 --- a/src/HOL/Library/Convex.thy	Thu Nov 05 10:35:37 2015 +0100
     8.2 +++ b/src/HOL/Library/Convex.thy	Thu Nov 05 10:39:49 2015 +0100
     8.3 @@ -883,7 +883,7 @@
     8.4    fix t x y :: real
     8.5    assume t: "t > 0" "t < 1" and xy: "x \<in> A" "y \<in> A" "x < y"
     8.6    def z \<equiv> "(1 - t) * x + t * y"
     8.7 -  with `connected A` and xy have ivl: "{x..y} \<subseteq> A" using connected_contains_Icc by blast
     8.8 +  with \<open>connected A\<close> and xy have ivl: "{x..y} \<subseteq> A" using connected_contains_Icc by blast
     8.9    
    8.10    from xy t have xz: "z > x" by (simp add: z_def algebra_simps)
    8.11    have "y - z = (1 - t) * (y - x)" by (simp add: z_def algebra_simps)
     9.1 --- a/src/HOL/Library/Countable_Set_Type.thy	Thu Nov 05 10:35:37 2015 +0100
     9.2 +++ b/src/HOL/Library/Countable_Set_Type.thy	Thu Nov 05 10:39:49 2015 +0100
     9.3 @@ -369,11 +369,11 @@
     9.4  
     9.5  subsection \<open>Additional lemmas\<close>
     9.6  
     9.7 -subsubsection \<open>@{text cempty}\<close>
     9.8 +subsubsection \<open>\<open>cempty\<close>\<close>
     9.9  
    9.10  lemma cemptyE [elim!]: "cin a cempty \<Longrightarrow> P" by simp
    9.11  
    9.12 -subsubsection \<open>@{text cinsert}\<close>
    9.13 +subsubsection \<open>\<open>cinsert\<close>\<close>
    9.14  
    9.15  lemma countable_insert_iff: "countable (insert x A) \<longleftrightarrow> countable A"
    9.16  by (metis Diff_eq_empty_iff countable_empty countable_insert subset_insertI uncountable_minus_countable)
    9.17 @@ -386,7 +386,7 @@
    9.18  lemma mk_disjoint_cinsert: "cin a A \<Longrightarrow> \<exists>B. A = cinsert a B \<and> \<not> cin a B"
    9.19    by (rule exI[where x = "cDiff A (csingle a)"]) blast
    9.20  
    9.21 -subsubsection \<open>@{text cimage}\<close>
    9.22 +subsubsection \<open>\<open>cimage\<close>\<close>
    9.23  
    9.24  lemma subset_cimage_iff: "csubset_eq B (cimage f A) \<longleftrightarrow> (\<exists>AA. csubset_eq AA A \<and> B = cimage f AA)"
    9.25  by transfer (metis countable_subset image_mono mem_Collect_eq subset_imageE) 
    10.1 --- a/src/HOL/Library/DAList.thy	Thu Nov 05 10:35:37 2015 +0100
    10.2 +++ b/src/HOL/Library/DAList.thy	Thu Nov 05 10:39:49 2015 +0100
    10.3 @@ -17,7 +17,7 @@
    10.4    by (induct xs) auto
    10.5  
    10.6  
    10.7 -subsection \<open>Type @{text "('key, 'value) alist" }\<close>
    10.8 +subsection \<open>Type \<open>('key, 'value) alist\<close>\<close>
    10.9  
   10.10  typedef ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. (distinct \<circ> map fst) xs}"
   10.11    morphisms impl_of Alist
    11.1 --- a/src/HOL/Library/DAList_Multiset.thy	Thu Nov 05 10:35:37 2015 +0100
    11.2 +++ b/src/HOL/Library/DAList_Multiset.thy	Thu Nov 05 10:39:49 2015 +0100
    11.3 @@ -206,8 +206,8 @@
    11.4  lemma mset_eq [code]: "HOL.equal (m1::'a::equal multiset) m2 \<longleftrightarrow> m1 \<le># m2 \<and> m2 \<le># m1"
    11.5    by (metis equal_multiset_def subset_mset.eq_iff)
    11.6  
    11.7 -text \<open>By default the code for @{text "<"} is @{prop"xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> xs = ys"}.
    11.8 -With equality implemented by @{text"\<le>"}, this leads to three calls of  @{text"\<le>"}.
    11.9 +text \<open>By default the code for \<open><\<close> is @{prop"xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> xs = ys"}.
   11.10 +With equality implemented by \<open>\<le>\<close>, this leads to three calls of  \<open>\<le>\<close>.
   11.11  Here is a more efficient version:\<close>
   11.12  lemma mset_less[code]: "xs <# (ys :: 'a multiset) \<longleftrightarrow> xs \<le># ys \<and> \<not> ys \<le># xs"
   11.13    by (rule subset_mset.less_le_not_le)
    12.1 --- a/src/HOL/Library/Debug.thy	Thu Nov 05 10:35:37 2015 +0100
    12.2 +++ b/src/HOL/Library/Debug.thy	Thu Nov 05 10:39:49 2015 +0100
    12.3 @@ -36,7 +36,7 @@
    12.4  
    12.5  code_printing
    12.6    constant Debug.trace \<rightharpoonup> (Eval) "Output.tracing"
    12.7 -| constant Debug.flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" -- \<open>note indirection via antiquotation\<close>
    12.8 +| constant Debug.flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" \<comment> \<open>note indirection via antiquotation\<close>
    12.9  | constant Debug.timing \<rightharpoonup> (Eval) "Timing.timeap'_msg"
   12.10  
   12.11  code_reserved Eval Output Timing
    13.1 --- a/src/HOL/Library/Extended_Real.thy	Thu Nov 05 10:35:37 2015 +0100
    13.2 +++ b/src/HOL/Library/Extended_Real.thy	Thu Nov 05 10:39:49 2015 +0100
    13.3 @@ -14,7 +14,7 @@
    13.4  text \<open>
    13.5  
    13.6  This should be part of @{theory Extended_Nat} or @{theory Order_Continuity}, but then the
    13.7 -AFP-entry @{text "Jinja_Thread"} fails, as it does overload certain named from @{theory Complex_Main}.
    13.8 +AFP-entry \<open>Jinja_Thread\<close> fails, as it does overload certain named from @{theory Complex_Main}.
    13.9  
   13.10  \<close>
   13.11  
   13.12 @@ -3613,7 +3613,7 @@
   13.13    shows "inverse -- x --> inverse x"
   13.14  proof (cases x)
   13.15    case (real r)
   13.16 -  with `0 < x` have **: "(\<lambda>x. ereal (inverse x)) -- r --> ereal (inverse r)"
   13.17 +  with \<open>0 < x\<close> have **: "(\<lambda>x. ereal (inverse x)) -- r --> ereal (inverse r)"
   13.18      by (auto intro!: tendsto_inverse)
   13.19    from real \<open>0 < x\<close> show ?thesis
   13.20      by (auto simp: at_ereal tendsto_compose_filtermap[symmetric] eventually_at_filter
    14.1 --- a/src/HOL/Library/FSet.thy	Thu Nov 05 10:35:37 2015 +0100
    14.2 +++ b/src/HOL/Library/FSet.thy	Thu Nov 05 10:39:49 2015 +0100
    14.3 @@ -445,12 +445,12 @@
    14.4  
    14.5  subsection \<open>Additional lemmas\<close>
    14.6  
    14.7 -subsubsection \<open>@{text fsingleton}\<close>
    14.8 +subsubsection \<open>\<open>fsingleton\<close>\<close>
    14.9  
   14.10  lemmas fsingletonE = fsingletonD [elim_format]
   14.11  
   14.12  
   14.13 -subsubsection \<open>@{text femepty}\<close>
   14.14 +subsubsection \<open>\<open>femepty\<close>\<close>
   14.15  
   14.16  lemma fempty_ffilter[simp]: "ffilter (\<lambda>_. False) A = {||}"
   14.17  by transfer auto
   14.18 @@ -460,7 +460,7 @@
   14.19    by simp
   14.20  
   14.21  
   14.22 -subsubsection \<open>@{text fset}\<close>
   14.23 +subsubsection \<open>\<open>fset\<close>\<close>
   14.24  
   14.25  lemmas fset_simps[simp] = bot_fset.rep_eq finsert.rep_eq
   14.26  
   14.27 @@ -483,7 +483,7 @@
   14.28  lemmas minus_fset[simp] = minus_fset.rep_eq
   14.29  
   14.30  
   14.31 -subsubsection \<open>@{text filter_fset}\<close>
   14.32 +subsubsection \<open>\<open>filter_fset\<close>\<close>
   14.33  
   14.34  lemma subset_ffilter: 
   14.35    "ffilter P A |\<subseteq>| ffilter Q A = (\<forall> x. x |\<in>| A \<longrightarrow> P x \<longrightarrow> Q x)"
   14.36 @@ -499,7 +499,7 @@
   14.37    unfolding less_fset_def by (auto simp add: subset_ffilter eq_ffilter)
   14.38  
   14.39  
   14.40 -subsubsection \<open>@{text finsert}\<close>
   14.41 +subsubsection \<open>\<open>finsert\<close>\<close>
   14.42  
   14.43  (* FIXME, transferred doesn't work here *)
   14.44  lemma set_finsert:
   14.45 @@ -511,7 +511,7 @@
   14.46    by (rule_tac x = "A |-| {|a|}" in exI, blast)
   14.47  
   14.48  
   14.49 -subsubsection \<open>@{text fimage}\<close>
   14.50 +subsubsection \<open>\<open>fimage\<close>\<close>
   14.51  
   14.52  lemma subset_fimage_iff: "(B |\<subseteq>| f|`|A) = (\<exists> AA. AA |\<subseteq>| A \<and> B = f|`|AA)"
   14.53  by transfer (metis mem_Collect_eq rev_finite_subset subset_image_iff)
   14.54 @@ -548,7 +548,7 @@
   14.55  end
   14.56  
   14.57  
   14.58 -subsubsection \<open>@{text fcard}\<close>
   14.59 +subsubsection \<open>\<open>fcard\<close>\<close>
   14.60  
   14.61  (* FIXME: improve transferred to handle bounded meta quantification *)
   14.62  
   14.63 @@ -631,7 +631,7 @@
   14.64  by transfer (rule card_psubset)
   14.65  
   14.66  
   14.67 -subsubsection \<open>@{text ffold}\<close>
   14.68 +subsubsection \<open>\<open>ffold\<close>\<close>
   14.69  
   14.70  (* FIXME: improve transferred to handle bounded meta quantification *)
   14.71  
    15.1 --- a/src/HOL/Library/FinFun.thy	Thu Nov 05 10:35:37 2015 +0100
    15.2 +++ b/src/HOL/Library/FinFun.thy	Thu Nov 05 10:39:49 2015 +0100
    15.3 @@ -17,7 +17,7 @@
    15.4  \<close>
    15.5  
    15.6  
    15.7 -subsection \<open>The @{text "map_default"} operation\<close>
    15.8 +subsection \<open>The \<open>map_default\<close> operation\<close>
    15.9  
   15.10  definition map_default :: "'b \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
   15.11  where "map_default b f a \<equiv> case f a of None \<Rightarrow> b | Some b' \<Rightarrow> b'"
   15.12 @@ -307,7 +307,7 @@
   15.13  
   15.14  quickcheck_generator finfun constructors: finfun_update_code, "finfun_const :: 'b \<Rightarrow> 'a \<Rightarrow>f 'b"
   15.15  
   15.16 -subsection \<open>@{text "finfun_update"} as instance of @{text "comp_fun_commute"}\<close>
   15.17 +subsection \<open>\<open>finfun_update\<close> as instance of \<open>comp_fun_commute\<close>\<close>
   15.18  
   15.19  interpretation finfun_update: comp_fun_commute "\<lambda>a f. f(a :: 'a $:= b')"
   15.20    including finfun
   15.21 @@ -1525,7 +1525,7 @@
   15.22  instance by intro_classes (simp add: card_UNIV_finfun_def card_UNIV Let_def card_UNIV_finfun)
   15.23  end
   15.24  
   15.25 -text \<open>Deactivate syntax again. Import theory @{text FinFun_Syntax} to reactivate it again\<close>
   15.26 +text \<open>Deactivate syntax again. Import theory \<open>FinFun_Syntax\<close> to reactivate it again\<close>
   15.27  
   15.28  no_type_notation
   15.29    finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
    16.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Thu Nov 05 10:35:37 2015 +0100
    16.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Thu Nov 05 10:39:49 2015 +0100
    16.3 @@ -1323,7 +1323,7 @@
    16.4  
    16.5  subsubsection \<open>Rule 3\<close>
    16.6  
    16.7 -text \<open>Rule 3 is trivial and is given by @{text fps_times_def}.\<close>
    16.8 +text \<open>Rule 3 is trivial and is given by \<open>fps_times_def\<close>.\<close>
    16.9  
   16.10  
   16.11  subsubsection \<open>Rule 5 --- summation and "division" by (1 - X)\<close>
   16.12 @@ -3774,7 +3774,7 @@
   16.13          unfolding eventually_nhds
   16.14          apply clarsimp
   16.15          apply (rule FalseE)
   16.16 -        apply auto -- \<open>slow\<close>
   16.17 +        apply auto \<comment> \<open>slow\<close>
   16.18          done
   16.19        then obtain i where "inverse (2 ^ i) < e"
   16.20          by (auto simp: eventually_sequentially)
    17.1 --- a/src/HOL/Library/FuncSet.thy	Thu Nov 05 10:35:37 2015 +0100
    17.2 +++ b/src/HOL/Library/FuncSet.thy	Thu Nov 05 10:39:49 2015 +0100
    17.3 @@ -226,7 +226,7 @@
    17.4  
    17.5  subsection \<open>Bijections Between Sets\<close>
    17.6  
    17.7 -text \<open>The definition of @{const bij_betw} is in @{text "Fun.thy"}, but most of
    17.8 +text \<open>The definition of @{const bij_betw} is in \<open>Fun.thy\<close>, but most of
    17.9  the theorems belong here, or need at least @{term Hilbert_Choice}.\<close>
   17.10  
   17.11  lemma bij_betwI:
    18.1 --- a/src/HOL/Library/Function_Growth.thy	Thu Nov 05 10:35:37 2015 +0100
    18.2 +++ b/src/HOL/Library/Function_Growth.thy	Thu Nov 05 10:39:49 2015 +0100
    18.3 @@ -12,39 +12,39 @@
    18.4  text \<open>
    18.5    When comparing growth of functions in computer science, it is common to adhere
    18.6    on Landau Symbols (``O-Notation'').  However these come at the cost of notational
    18.7 -  oddities, particularly writing @{text "f = O(g)"} for @{text "f \<in> O(g)"} etc.
    18.8 +  oddities, particularly writing \<open>f = O(g)\<close> for \<open>f \<in> O(g)\<close> etc.
    18.9    
   18.10    Here we suggest a different way, following Hardy (G.~H.~Hardy and J.~E.~Littlewood,
   18.11    Some problems of Diophantine approximation, Acta Mathematica 37 (1914), p.~225).
   18.12 -  We establish a quasi order relation @{text "\<lesssim>"} on functions such that
   18.13 -  @{text "f \<lesssim> g \<longleftrightarrow> f \<in> O(g)"}.  From a didactic point of view, this does not only
   18.14 +  We establish a quasi order relation \<open>\<lesssim>\<close> on functions such that
   18.15 +  \<open>f \<lesssim> g \<longleftrightarrow> f \<in> O(g)\<close>.  From a didactic point of view, this does not only
   18.16    avoid the notational oddities mentioned above but also emphasizes the key insight
   18.17    of a growth hierarchy of functions:
   18.18 -  @{text "(\<lambda>n. 0) \<lesssim> (\<lambda>n. k) \<lesssim> Discrete.log \<lesssim> Discrete.sqrt \<lesssim> id \<lesssim> \<dots>"}.
   18.19 +  \<open>(\<lambda>n. 0) \<lesssim> (\<lambda>n. k) \<lesssim> Discrete.log \<lesssim> Discrete.sqrt \<lesssim> id \<lesssim> \<dots>\<close>.
   18.20  \<close>
   18.21  
   18.22  subsection \<open>Model\<close>
   18.23  
   18.24  text \<open>
   18.25 -  Our growth functions are of type @{text "\<nat> \<Rightarrow> \<nat>"}.  This is different
   18.26 -  to the usual conventions for Landau symbols for which @{text "\<real> \<Rightarrow> \<real>"}
   18.27 -  would be appropriate, but we argue that @{text "\<real> \<Rightarrow> \<real>"} is more
   18.28 +  Our growth functions are of type \<open>\<nat> \<Rightarrow> \<nat>\<close>.  This is different
   18.29 +  to the usual conventions for Landau symbols for which \<open>\<real> \<Rightarrow> \<real>\<close>
   18.30 +  would be appropriate, but we argue that \<open>\<real> \<Rightarrow> \<real>\<close> is more
   18.31    appropriate for analysis, whereas our setting is discrete.
   18.32  
   18.33 -  Note that we also restrict the additional coefficients to @{text \<nat>}, something
   18.34 +  Note that we also restrict the additional coefficients to \<open>\<nat>\<close>, something
   18.35    we discuss at the particular definitions.
   18.36  \<close>
   18.37  
   18.38 -subsection \<open>The @{text "\<lesssim>"} relation\<close>
   18.39 +subsection \<open>The \<open>\<lesssim>\<close> relation\<close>
   18.40  
   18.41  definition less_eq_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<lesssim>" 50)
   18.42  where
   18.43    "f \<lesssim> g \<longleftrightarrow> (\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m)"
   18.44  
   18.45  text \<open>
   18.46 -  This yields @{text "f \<lesssim> g \<longleftrightarrow> f \<in> O(g)"}.  Note that @{text c} is restricted to
   18.47 -  @{text \<nat>}.  This does not pose any problems since if @{text "f \<in> O(g)"} holds for
   18.48 -  a @{text "c \<in> \<real>"}, it also holds for @{text "\<lceil>c\<rceil> \<in> \<nat>"} by transitivity.
   18.49 +  This yields \<open>f \<lesssim> g \<longleftrightarrow> f \<in> O(g)\<close>.  Note that \<open>c\<close> is restricted to
   18.50 +  \<open>\<nat>\<close>.  This does not pose any problems since if \<open>f \<in> O(g)\<close> holds for
   18.51 +  a \<open>c \<in> \<real>\<close>, it also holds for \<open>\<lceil>c\<rceil> \<in> \<nat>\<close> by transitivity.
   18.52  \<close>
   18.53  
   18.54  lemma less_eq_funI [intro?]:
   18.55 @@ -68,7 +68,7 @@
   18.56    using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast
   18.57  
   18.58  
   18.59 -subsection \<open>The @{text "\<approx>"} relation, the equivalence relation induced by @{text "\<lesssim>"}\<close>
   18.60 +subsection \<open>The \<open>\<approx>\<close> relation, the equivalence relation induced by \<open>\<lesssim>\<close>\<close>
   18.61  
   18.62  definition equiv_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<cong>" 50)
   18.63  where
   18.64 @@ -76,8 +76,8 @@
   18.65      (\<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)"
   18.66  
   18.67  text \<open>
   18.68 -  This yields @{text "f \<cong> g \<longleftrightarrow> f \<in> \<Theta>(g)"}.  Concerning @{text "c\<^sub>1"} and @{text "c\<^sub>2"}
   18.69 -  restricted to @{typ nat}, see note above on @{text "(\<lesssim>)"}.
   18.70 +  This yields \<open>f \<cong> g \<longleftrightarrow> f \<in> \<Theta>(g)\<close>.  Concerning \<open>c\<^sub>1\<close> and \<open>c\<^sub>2\<close>
   18.71 +  restricted to @{typ nat}, see note above on \<open>(\<lesssim>)\<close>.
   18.72  \<close>
   18.73  
   18.74  lemma equiv_funI [intro?]:
   18.75 @@ -105,7 +105,7 @@
   18.76    using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast
   18.77  
   18.78  
   18.79 -subsection \<open>The @{text "\<prec>"} relation, the strict part of @{text "\<lesssim>"}\<close>
   18.80 +subsection \<open>The \<open>\<prec>\<close> relation, the strict part of \<open>\<lesssim>\<close>\<close>
   18.81  
   18.82  definition less_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<prec>" 50)
   18.83  where
   18.84 @@ -147,18 +147,18 @@
   18.85    using assms unfolding less_fun_def linorder_not_less [symmetric] by blast
   18.86  
   18.87  text \<open>
   18.88 -  I did not find a proof for @{text "f \<prec> g \<longleftrightarrow> f \<in> o(g)"}.  Maybe this only
   18.89 -  holds if @{text f} and/or @{text g} are of a certain class of functions.
   18.90 -  However @{text "f \<in> o(g) \<longrightarrow> f \<prec> g"} is provable, and this yields a
   18.91 +  I did not find a proof for \<open>f \<prec> g \<longleftrightarrow> f \<in> o(g)\<close>.  Maybe this only
   18.92 +  holds if \<open>f\<close> and/or \<open>g\<close> are of a certain class of functions.
   18.93 +  However \<open>f \<in> o(g) \<longrightarrow> f \<prec> g\<close> is provable, and this yields a
   18.94    handy introduction rule.
   18.95  
   18.96 -  Note that D. Knuth ignores @{text o} altogether.  So what \dots
   18.97 +  Note that D. Knuth ignores \<open>o\<close> altogether.  So what \dots
   18.98  
   18.99 -  Something still has to be said about the coefficient @{text c} in
  18.100 -  the definition of @{text "(\<prec>)"}.  In the typical definition of @{text o},
  18.101 -  it occurs on the \emph{right} hand side of the @{text "(>)"}.  The reason
  18.102 -  is that the situation is dual to the definition of @{text O}: the definition
  18.103 -  works since @{text c} may become arbitrary small.  Since this is not possible
  18.104 +  Something still has to be said about the coefficient \<open>c\<close> in
  18.105 +  the definition of \<open>(\<prec>)\<close>.  In the typical definition of \<open>o\<close>,
  18.106 +  it occurs on the \emph{right} hand side of the \<open>(>)\<close>.  The reason
  18.107 +  is that the situation is dual to the definition of \<open>O\<close>: the definition
  18.108 +  works since \<open>c\<close> may become arbitrary small.  Since this is not possible
  18.109    within @{term \<nat>}, we push the coefficient to the left hand side instead such
  18.110    that it become arbitrary big instead.
  18.111  \<close>
  18.112 @@ -187,9 +187,9 @@
  18.113  qed
  18.114  
  18.115  
  18.116 -subsection \<open>@{text "\<lesssim>"} is a preorder\<close>
  18.117 +subsection \<open>\<open>\<lesssim>\<close> is a preorder\<close>
  18.118  
  18.119 -text \<open>This yields all lemmas relating @{text "\<lesssim>"}, @{text "\<prec>"} and @{text "\<cong>"}.\<close>
  18.120 +text \<open>This yields all lemmas relating \<open>\<lesssim>\<close>, \<open>\<prec>\<close> and \<open>\<cong>\<close>.\<close>
  18.121  
  18.122  interpretation fun_order: preorder_equiv less_eq_fun less_fun
  18.123    rewrites "preorder_equiv.equiv less_eq_fun = equiv_fun"
    19.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Thu Nov 05 10:35:37 2015 +0100
    19.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Thu Nov 05 10:39:49 2015 +0100
    19.3 @@ -149,7 +149,7 @@
    19.4      unfolding linorder_not_le[symmetric] by blast
    19.5  qed
    19.6  
    19.7 -text \<open>Hence we can always reduce modulus of @{text "1 + b z^n"} if nonzero\<close>
    19.8 +text \<open>Hence we can always reduce modulus of \<open>1 + b z^n\<close> if nonzero\<close>
    19.9  lemma reduce_poly_simple:
   19.10    assumes b: "b \<noteq> 0"
   19.11      and n: "n \<noteq> 0"
    20.1 --- a/src/HOL/Library/Infinite_Set.thy	Thu Nov 05 10:35:37 2015 +0100
    20.2 +++ b/src/HOL/Library/Infinite_Set.thy	Thu Nov 05 10:39:49 2015 +0100
    20.3 @@ -13,7 +13,7 @@
    20.4  text \<open>
    20.5    Some elementary facts about infinite sets, mostly by Stephan Merz.
    20.6    Beware! Because "infinite" merely abbreviates a negation, these
    20.7 -  lemmas may not work well with @{text "blast"}.
    20.8 +  lemmas may not work well with \<open>blast\<close>.
    20.9  \<close>
   20.10  
   20.11  abbreviation infinite :: "'a set \<Rightarrow> bool"
   20.12 @@ -96,7 +96,7 @@
   20.13  
   20.14  text \<open>
   20.15    For a set of natural numbers to be infinite, it is enough to know
   20.16 -  that for any number larger than some @{text k}, there is some larger
   20.17 +  that for any number larger than some \<open>k\<close>, there is some larger
   20.18    number that is an element of the set.
   20.19  \<close>
   20.20  
    21.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Thu Nov 05 10:35:37 2015 +0100
    21.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Thu Nov 05 10:39:49 2015 +0100
    21.3 @@ -30,7 +30,7 @@
    21.4    shows "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
    21.5    by (rule antisym) (auto intro!: INF_greatest INF_lower2)
    21.6  
    21.7 -subsubsection \<open>@{text Liminf} and @{text Limsup}\<close>
    21.8 +subsubsection \<open>\<open>Liminf\<close> and \<open>Limsup\<close>\<close>
    21.9  
   21.10  definition Liminf :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
   21.11    "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)"
    22.1 --- a/src/HOL/Library/ListVector.thy	Thu Nov 05 10:35:37 2015 +0100
    22.2 +++ b/src/HOL/Library/ListVector.thy	Thu Nov 05 10:39:49 2015 +0100
    22.3 @@ -18,7 +18,7 @@
    22.4  lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs"
    22.5  by (induct xs) simp_all
    22.6  
    22.7 -subsection \<open>@{text"+"} and @{text"-"}\<close>
    22.8 +subsection \<open>\<open>+\<close> and \<open>-\<close>\<close>
    22.9  
   22.10  fun zipwith0 :: "('a::zero \<Rightarrow> 'b::zero \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
   22.11  where
    23.1 --- a/src/HOL/Library/Lub_Glb.thy	Thu Nov 05 10:35:37 2015 +0100
    23.2 +++ b/src/HOL/Library/Lub_Glb.thy	Thu Nov 05 10:39:49 2015 +0100
    23.3 @@ -17,7 +17,7 @@
    23.4    where "x <=* S = (ALL y: S. x \<le> y)"
    23.5  
    23.6  
    23.7 -subsection \<open>Rules for the Relations @{text "*<="} and @{text "<=*"}\<close>
    23.8 +subsection \<open>Rules for the Relations \<open>*<=\<close> and \<open><=*\<close>\<close>
    23.9  
   23.10  lemma setleI: "ALL y: S. y \<le> x \<Longrightarrow> S *<= x"
   23.11    by (simp add: setle_def)
    24.1 --- a/src/HOL/Library/Mapping.thy	Thu Nov 05 10:35:37 2015 +0100
    24.2 +++ b/src/HOL/Library/Mapping.thy	Thu Nov 05 10:39:49 2015 +0100
    24.3 @@ -10,7 +10,7 @@
    24.4  
    24.5  subsection \<open>Parametricity transfer rules\<close>
    24.6  
    24.7 -lemma map_of_foldr: -- \<open>FIXME move\<close>
    24.8 +lemma map_of_foldr: \<comment> \<open>FIXME move\<close>
    24.9    "map_of xs = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) xs Map.empty"
   24.10    using map_add_map_of_foldr [of Map.empty] by auto
   24.11  
   24.12 @@ -107,7 +107,7 @@
   24.13    is "\<lambda>m k. m k" parametric lookup_parametric .
   24.14  
   24.15  declare [[code drop: Mapping.lookup]]
   24.16 -setup \<open>Code.add_default_eqn @{thm Mapping.lookup.abs_eq}\<close> -- \<open>FIXME lifting\<close>
   24.17 +setup \<open>Code.add_default_eqn @{thm Mapping.lookup.abs_eq}\<close> \<comment> \<open>FIXME lifting\<close>
   24.18  
   24.19  lift_definition update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping"
   24.20    is "\<lambda>k v m. m(k \<mapsto> v)" parametric update_parametric .
    25.1 --- a/src/HOL/Library/Multiset.thy	Thu Nov 05 10:35:37 2015 +0100
    25.2 +++ b/src/HOL/Library/Multiset.thy	Thu Nov 05 10:39:49 2015 +0100
    25.3 @@ -809,12 +809,11 @@
    25.4  text \<open>
    25.5    A note on code generation: When defining some function containing a
    25.6    subterm @{term "fold_mset F"}, code generation is not automatic. When
    25.7 -  interpreting locale @{text left_commutative} with @{text F}, the
    25.8 +  interpreting locale \<open>left_commutative\<close> with \<open>F\<close>, the
    25.9    would be code thms for @{const fold_mset} become thms like
   25.10 -  @{term "fold_mset F z {#} = z"} where @{text F} is not a pattern but
   25.11 +  @{term "fold_mset F z {#} = z"} where \<open>F\<close> is not a pattern but
   25.12    contains defined symbols, i.e.\ is not a code thm. Hence a separate
   25.13 -  constant with its own code thms needs to be introduced for @{text
   25.14 -  F}. See the image operator below.
   25.15 +  constant with its own code thms needs to be introduced for \<open>F\<close>. See the image operator below.
   25.16  \<close>
   25.17  
   25.18  
   25.19 @@ -1083,7 +1082,7 @@
   25.20    qed
   25.21    then show "PROP ?P" "PROP ?Q" "PROP ?R"
   25.22    by (auto elim!: Set.set_insert)
   25.23 -qed -- \<open>TODO: maybe define @{const mset_set} also in terms of @{const Abs_multiset}\<close>
   25.24 +qed \<comment> \<open>TODO: maybe define @{const mset_set} also in terms of @{const Abs_multiset}\<close>
   25.25  
   25.26  lemma elem_mset_set[simp, intro]: "finite A \<Longrightarrow> x \<in># mset_set A \<longleftrightarrow> x \<in> A"
   25.27    by (induct A rule: finite_induct) simp_all
   25.28 @@ -1349,7 +1348,7 @@
   25.29  
   25.30  text \<open>
   25.31    This lemma shows which properties suffice to show that a function
   25.32 -  @{text "f"} with @{text "f xs = ys"} behaves like sort.
   25.33 +  \<open>f\<close> with \<open>f xs = ys\<close> behaves like sort.
   25.34  \<close>
   25.35  
   25.36  lemma properties_for_sort_key:
   25.37 @@ -2106,7 +2105,7 @@
   25.38  
   25.39  declare sorted_list_of_multiset_mset [code]
   25.40  
   25.41 -lemma [code]: -- \<open>not very efficient, but representation-ignorant!\<close>
   25.42 +lemma [code]: \<comment> \<open>not very efficient, but representation-ignorant!\<close>
   25.43    "mset_set A = mset (sorted_list_of_set A)"
   25.44    apply (cases "finite A")
   25.45    apply simp_all
    26.1 --- a/src/HOL/Library/Numeral_Type.thy	Thu Nov 05 10:35:37 2015 +0100
    26.2 +++ b/src/HOL/Library/Numeral_Type.thy	Thu Nov 05 10:39:49 2015 +0100
    26.3 @@ -182,7 +182,7 @@
    26.4  subsection \<open>Ring class instances\<close>
    26.5  
    26.6  text \<open>
    26.7 -  Unfortunately @{text ring_1} instance is not possible for
    26.8 +  Unfortunately \<open>ring_1\<close> instance is not possible for
    26.9    @{typ num1}, since 0 and 1 are not distinct.
   26.10  \<close>
   26.11  
    27.1 --- a/src/HOL/Library/Old_Datatype.thy	Thu Nov 05 10:35:37 2015 +0100
    27.2 +++ b/src/HOL/Library/Old_Datatype.thy	Thu Nov 05 10:39:49 2015 +0100
    27.3 @@ -21,7 +21,7 @@
    27.4    morphisms Rep_Node Abs_Node
    27.5    unfolding Node_def by auto
    27.6  
    27.7 -text\<open>Datatypes will be represented by sets of type @{text node}\<close>
    27.8 +text\<open>Datatypes will be represented by sets of type \<open>node\<close>\<close>
    27.9  
   27.10  type_synonym 'a item        = "('a, unit) node set"
   27.11  type_synonym ('a, 'b) dtree = "('a, 'b) node set"
    28.1 --- a/src/HOL/Library/Old_SMT.thy	Thu Nov 05 10:35:37 2015 +0100
    28.2 +++ b/src/HOL/Library/Old_SMT.thy	Thu Nov 05 10:39:49 2015 +0100
    28.3 @@ -51,7 +51,7 @@
    28.4  definition weight :: "int \<Rightarrow> bool \<Rightarrow> bool" where "weight _ P = P"
    28.5  
    28.6  text \<open>
    28.7 -Weights must be non-negative.  The value @{text 0} is equivalent to providing
    28.8 +Weights must be non-negative.  The value \<open>0\<close> is equivalent to providing
    28.9  no weight at all.
   28.10  
   28.11  Weights should only be used at quantifiers and only inside triggers (if the
   28.12 @@ -150,7 +150,7 @@
   28.13  
   28.14  text \<open>
   28.15  The current configuration can be printed by the command
   28.16 -@{text old_smt_status}, which shows the values of most options.
   28.17 +\<open>old_smt_status\<close>, which shows the values of most options.
   28.18  \<close>
   28.19  
   28.20  
   28.21 @@ -158,14 +158,14 @@
   28.22  subsection \<open>General configuration options\<close>
   28.23  
   28.24  text \<open>
   28.25 -The option @{text old_smt_solver} can be used to change the target SMT
   28.26 -solver.  The possible values can be obtained from the @{text old_smt_status}
   28.27 +The option \<open>old_smt_solver\<close> can be used to change the target SMT
   28.28 +solver.  The possible values can be obtained from the \<open>old_smt_status\<close>
   28.29  command.
   28.30  
   28.31  Due to licensing restrictions, Yices and Z3 are not installed/enabled
   28.32  by default.  Z3 is free for non-commercial applications and can be enabled
   28.33 -by setting the @{text OLD_Z3_NON_COMMERCIAL} environment variable to
   28.34 -@{text yes}.
   28.35 +by setting the \<open>OLD_Z3_NON_COMMERCIAL\<close> environment variable to
   28.36 +\<open>yes\<close>.
   28.37  \<close>
   28.38  
   28.39  declare [[ old_smt_solver = z3 ]]
   28.40 @@ -242,7 +242,7 @@
   28.41  subsection \<open>Certificates\<close>
   28.42  
   28.43  text \<open>
   28.44 -By setting the option @{text old_smt_certificates} to the name of a file,
   28.45 +By setting the option \<open>old_smt_certificates\<close> to the name of a file,
   28.46  all following applications of an SMT solver a cached in that file.
   28.47  Any further application of the same SMT solver (using the very same
   28.48  configuration) re-uses the cached certificate instead of invoking the
   28.49 @@ -250,7 +250,7 @@
   28.50  
   28.51  The filename should be given as an explicit path.  It is good
   28.52  practice to use the name of the current theory (with ending
   28.53 -@{text ".certs"} instead of @{text ".thy"}) as the certificates file.
   28.54 +\<open>.certs\<close> instead of \<open>.thy\<close>) as the certificates file.
   28.55  Certificate files should be used at most once in a certain theory context,
   28.56  to avoid race conditions with other concurrent accesses.
   28.57  \<close>
   28.58 @@ -258,11 +258,11 @@
   28.59  declare [[ old_smt_certificates = "" ]]
   28.60  
   28.61  text \<open>
   28.62 -The option @{text old_smt_read_only_certificates} controls whether only
   28.63 +The option \<open>old_smt_read_only_certificates\<close> controls whether only
   28.64  stored certificates are should be used or invocation of an SMT solver
   28.65 -is allowed.  When set to @{text true}, no SMT solver will ever be
   28.66 +is allowed.  When set to \<open>true\<close>, no SMT solver will ever be
   28.67  invoked and only the existing certificates found in the configured
   28.68 -cache are used;  when set to @{text false} and there is no cached
   28.69 +cache are used;  when set to \<open>false\<close> and there is no cached
   28.70  certificate for some proposition, then the configured SMT solver is
   28.71  invoked.
   28.72  \<close>
   28.73 @@ -275,7 +275,7 @@
   28.74  
   28.75  text \<open>
   28.76  The SMT method, when applied, traces important information.  To
   28.77 -make it entirely silent, set the following option to @{text false}.
   28.78 +make it entirely silent, set the following option to \<open>false\<close>.
   28.79  \<close>
   28.80  
   28.81  declare [[ old_smt_verbose = true ]]
   28.82 @@ -283,7 +283,7 @@
   28.83  text \<open>
   28.84  For tracing the generated problem file given to the SMT solver as
   28.85  well as the returned result of the solver, the option
   28.86 -@{text old_smt_trace} should be set to @{text true}.
   28.87 +\<open>old_smt_trace\<close> should be set to \<open>true\<close>.
   28.88  \<close>
   28.89  
   28.90  declare [[ old_smt_trace = false ]]
   28.91 @@ -292,7 +292,7 @@
   28.92  From the set of assumptions given to the SMT solver, those assumptions
   28.93  used in the proof are traced when the following option is set to
   28.94  @{term true}.  This only works for Z3 when it runs in non-oracle mode
   28.95 -(see options @{text old_smt_solver} and @{text old_smt_oracle} above).
   28.96 +(see options \<open>old_smt_solver\<close> and \<open>old_smt_oracle\<close> above).
   28.97  \<close>
   28.98  
   28.99  declare [[ old_smt_trace_used_facts = false ]]
  28.100 @@ -304,9 +304,9 @@
  28.101  text \<open>
  28.102  Several prof rules of Z3 are not very well documented.  There are two
  28.103  lemma groups which can turn failing Z3 proof reconstruction attempts
  28.104 -into succeeding ones: the facts in @{text z3_rule} are tried prior to
  28.105 +into succeeding ones: the facts in \<open>z3_rule\<close> are tried prior to
  28.106  any implemented reconstruction procedure for all uncertain Z3 proof
  28.107 -rules;  the facts in @{text z3_simp} are only fed to invocations of
  28.108 +rules;  the facts in \<open>z3_simp\<close> are only fed to invocations of
  28.109  the simplifier when reconstructing theory-specific proof steps.
  28.110  \<close>
  28.111  
    29.1 --- a/src/HOL/Library/Omega_Words_Fun.thy	Thu Nov 05 10:35:37 2015 +0100
    29.2 +++ b/src/HOL/Library/Omega_Words_Fun.thy	Thu Nov 05 10:39:49 2015 +0100
    29.3 @@ -529,20 +529,20 @@
    29.4  proof -
    29.5    have "\<exists>k. range (suffix k x) \<subseteq> limit x"
    29.6    proof -
    29.7 -    -- "The set of letters that are not in the limit is certainly finite."
    29.8 +    \<comment> "The set of letters that are not in the limit is certainly finite."
    29.9      from fin have "finite (range x - limit x)"
   29.10        by simp
   29.11 -    -- "Moreover, any such letter occurs only finitely often"
   29.12 +    \<comment> "Moreover, any such letter occurs only finitely often"
   29.13      moreover
   29.14      have "\<forall>a \<in> range x - limit x. finite (x -` {a})"
   29.15        by (auto simp add: limit_vimage)
   29.16 -    -- "Thus, there are only finitely many occurrences of such letters."
   29.17 +    \<comment> "Thus, there are only finitely many occurrences of such letters."
   29.18      ultimately have "finite (UN a : range x - limit x. x -` {a})"
   29.19        by (blast intro: finite_UN_I)
   29.20 -    -- "Therefore these occurrences are within some initial interval."
   29.21 +    \<comment> "Therefore these occurrences are within some initial interval."
   29.22      then obtain k where "(UN a : range x - limit x. x -` {a}) \<subseteq> {..<k}"
   29.23        by (blast dest: finite_nat_bounded)
   29.24 -    -- "This is just the bound we are looking for."
   29.25 +    \<comment> "This is just the bound we are looking for."
   29.26      hence "\<forall>m. k \<le> m \<longrightarrow> x m \<in> limit x"
   29.27        by (auto simp add: limit_vimage)
   29.28      hence "range (suffix k x) \<subseteq> limit x"
   29.29 @@ -624,11 +624,11 @@
   29.30      fix a assume a: "a \<in> set w"
   29.31      then obtain k where k: "k < length w \<and> w!k = a"
   29.32        by (auto simp add: set_conv_nth)
   29.33 -    -- "the following bound is terrible, but it simplifies the proof"
   29.34 +    \<comment> "the following bound is terrible, but it simplifies the proof"
   29.35      from nempty k have "\<forall>m. w\<^sup>\<omega> ((Suc m)*(length w) + k) = a"
   29.36        by (simp add: mod_add_left_eq)
   29.37      moreover
   29.38 -    -- "why is the following so hard to prove??"
   29.39 +    \<comment> "why is the following so hard to prove??"
   29.40      have "\<forall>m. m < (Suc m)*(length w) + k"
   29.41      proof
   29.42        fix m
   29.43 @@ -661,7 +661,7 @@
   29.44  text \<open>
   29.45    The converse relation is not true in general: $f(a)$ can be in the
   29.46    limit of $f \circ w$ even though $a$ is not in the limit of $w$.
   29.47 -  However, @{text limit} commutes with renaming if the function is
   29.48 +  However, \<open>limit\<close> commutes with renaming if the function is
   29.49    injective. More generally, if $f(a)$ is the image of only finitely
   29.50    many elements, some of these must be in the limit of $w$.
   29.51  \<close>
   29.52 @@ -672,21 +672,21 @@
   29.53    shows "\<exists>a \<in> (f -` {x}). a \<in> limit w"
   29.54  proof (rule ccontr)
   29.55    assume contra: "\<not> ?thesis"
   29.56 -  -- "hence, every element in the pre-image occurs only finitely often"
   29.57 +  \<comment> "hence, every element in the pre-image occurs only finitely often"
   29.58    then have "\<forall>a \<in> (f -` {x}). finite {n. w n = a}"
   29.59      by (simp add: limit_def Inf_many_def)
   29.60 -  -- "so there are only finitely many occurrences of any such element"
   29.61 +  \<comment> "so there are only finitely many occurrences of any such element"
   29.62    with fin have "finite (\<Union> a \<in> (f -` {x}). {n. w n = a})"
   29.63      by auto
   29.64 -  -- \<open>these are precisely those positions where $x$ occurs in $f \circ w$\<close>
   29.65 +  \<comment> \<open>these are precisely those positions where $x$ occurs in $f \circ w$\<close>
   29.66    moreover
   29.67    have "(\<Union> a \<in> (f -` {x}). {n. w n = a}) = {n. f(w n) = x}"
   29.68      by auto
   29.69    ultimately
   29.70 -  -- "so $x$ can occur only finitely often in the translated word"
   29.71 +  \<comment> "so $x$ can occur only finitely often in the translated word"
   29.72    have "finite {n. f(w n) = x}"
   29.73      by simp
   29.74 -  -- \<open>\ldots\ which yields a contradiction\<close>
   29.75 +  \<comment> \<open>\ldots\ which yields a contradiction\<close>
   29.76    with x show "False"
   29.77      by (simp add: limit_def Inf_many_def)
   29.78  qed
    30.1 --- a/src/HOL/Library/Order_Continuity.thy	Thu Nov 05 10:35:37 2015 +0100
    30.2 +++ b/src/HOL/Library/Order_Continuity.thy	Thu Nov 05 10:39:49 2015 +0100
    30.3 @@ -29,8 +29,8 @@
    30.4    done
    30.5  
    30.6  text \<open>
    30.7 -  The name @{text continuous} is already taken in @{text "Complex_Main"}, so we use
    30.8 -  @{text "sup_continuous"} and @{text "inf_continuous"}. These names appear sometimes in literature
    30.9 +  The name \<open>continuous\<close> is already taken in \<open>Complex_Main\<close>, so we use
   30.10 +  \<open>sup_continuous\<close> and \<open>inf_continuous\<close>. These names appear sometimes in literature
   30.11    and have the advantage that these names are duals.
   30.12  \<close>
   30.13  
    31.1 --- a/src/HOL/Library/Permutation.thy	Thu Nov 05 10:35:37 2015 +0100
    31.2 +++ b/src/HOL/Library/Permutation.thy	Thu Nov 05 10:39:49 2015 +0100
    31.3 @@ -116,7 +116,7 @@
    31.4    apply (safe intro!: perm_append2)
    31.5    apply (rule append_perm_imp_perm)
    31.6    apply (rule perm_append_swap [THEN perm.trans])
    31.7 -    -- \<open>the previous step helps this @{text blast} call succeed quickly\<close>
    31.8 +    \<comment> \<open>the previous step helps this \<open>blast\<close> call succeed quickly\<close>
    31.9    apply (blast intro: perm_append_swap)
   31.10    done
   31.11  
    32.1 --- a/src/HOL/Library/Polynomial.thy	Thu Nov 05 10:35:37 2015 +0100
    32.2 +++ b/src/HOL/Library/Polynomial.thy	Thu Nov 05 10:39:49 2015 +0100
    32.3 @@ -50,7 +50,7 @@
    32.4    "tl (x ## xs) = xs"
    32.5    by (simp add: cCons_def)
    32.6  
    32.7 -subsection \<open>Definition of type @{text poly}\<close>
    32.8 +subsection \<open>Definition of type \<open>poly\<close>\<close>
    32.9  
   32.10  typedef (overloaded) 'a poly = "{f :: nat \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n. f n = 0}"
   32.11    morphisms coeff Abs_poly by (auto intro!: ALL_MOST)
   32.12 @@ -440,7 +440,7 @@
   32.13  
   32.14  definition poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a"
   32.15  where
   32.16 -  "poly p = fold_coeffs (\<lambda>a f x. a + x * f x) p (\<lambda>x. 0)" -- \<open>The Horner Schema\<close>
   32.17 +  "poly p = fold_coeffs (\<lambda>a f x. a + x * f x) p (\<lambda>x. 0)" \<comment> \<open>The Horner Schema\<close>
   32.18  
   32.19  lemma poly_0 [simp]:
   32.20    "poly 0 x = 0"
    33.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Nov 05 10:35:37 2015 +0100
    33.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Nov 05 10:39:49 2015 +0100
    33.3 @@ -177,7 +177,7 @@
    33.4  
    33.5  section \<open>Alternative list definitions\<close>
    33.6  
    33.7 -subsection \<open>Alternative rules for @{text length}\<close>
    33.8 +subsection \<open>Alternative rules for \<open>length\<close>\<close>
    33.9  
   33.10  definition size_list' :: "'a list => nat"
   33.11  where "size_list' = size"
   33.12 @@ -191,7 +191,7 @@
   33.13  declare size_list'_def[symmetric, code_pred_inline]
   33.14  
   33.15  
   33.16 -subsection \<open>Alternative rules for @{text list_all2}\<close>
   33.17 +subsection \<open>Alternative rules for \<open>list_all2\<close>\<close>
   33.18  
   33.19  lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"
   33.20  by auto
    34.1 --- a/src/HOL/Library/Quotient_Type.thy	Thu Nov 05 10:35:37 2015 +0100
    34.2 +++ b/src/HOL/Library/Quotient_Type.thy	Thu Nov 05 10:39:49 2015 +0100
    34.3 @@ -14,8 +14,8 @@
    34.4  
    34.5  subsection \<open>Equivalence relations and quotient types\<close>
    34.6  
    34.7 -text \<open>Type class @{text equiv} models equivalence relations
    34.8 -  @{text "\<sim> :: 'a \<Rightarrow> 'a \<Rightarrow> bool"}.\<close>
    34.9 +text \<open>Type class \<open>equiv\<close> models equivalence relations
   34.10 +  \<open>\<sim> :: 'a \<Rightarrow> 'a \<Rightarrow> bool\<close>.\<close>
   34.11  
   34.12  class eqv =
   34.13    fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infixl "\<sim>" 50)
   34.14 @@ -57,7 +57,7 @@
   34.15  
   34.16  end
   34.17  
   34.18 -text \<open>The quotient type @{text "'a quot"} consists of all \emph{equivalence
   34.19 +text \<open>The quotient type \<open>'a quot\<close> consists of all \emph{equivalence
   34.20    classes} over elements of the base type @{typ 'a}.\<close>
   34.21  
   34.22  definition (in eqv) "quot = {{x. a \<sim> x} | a. True}"
    35.1 --- a/src/HOL/Library/RBT_Impl.thy	Thu Nov 05 10:35:37 2015 +0100
    35.2 +++ b/src/HOL/Library/RBT_Impl.thy	Thu Nov 05 10:39:49 2015 +0100
    35.3 @@ -10,7 +10,7 @@
    35.4  begin
    35.5  
    35.6  text \<open>
    35.7 -  For applications, you should use theory @{text RBT} which defines
    35.8 +  For applications, you should use theory \<open>RBT\<close> which defines
    35.9    an abstract type of red-black tree obeying the invariant.
   35.10  \<close>
   35.11  
   35.12 @@ -305,7 +305,7 @@
   35.13    "inv1 Empty = True"
   35.14  | "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)"
   35.15  
   35.16 -primrec inv1l :: "('a, 'b) rbt \<Rightarrow> bool" -- \<open>Weaker version\<close>
   35.17 +primrec inv1l :: "('a, 'b) rbt \<Rightarrow> bool" \<comment> \<open>Weaker version\<close>
   35.18  where
   35.19    "inv1l Empty = True"
   35.20  | "inv1l (Branch c l k v r) = (inv1 l \<and> inv1 r)"
    36.1 --- a/src/HOL/Library/RBT_Mapping.thy	Thu Nov 05 10:35:37 2015 +0100
    36.2 +++ b/src/HOL/Library/RBT_Mapping.thy	Thu Nov 05 10:39:49 2015 +0100
    36.3 @@ -100,11 +100,11 @@
    36.4  text \<open>
    36.5    The type @{typ "('k, 'v) RBT_Impl.rbt"} denotes red-black trees with
    36.6    keys of type @{typ "'k"} and values of type @{typ "'v"}. To function
    36.7 -  properly, the key type musorted belong to the @{text "linorder"}
    36.8 +  properly, the key type musorted belong to the \<open>linorder\<close>
    36.9    class.
   36.10  
   36.11    A value @{term t} of this type is a valid red-black tree if it
   36.12 -  satisfies the invariant @{text "is_rbt t"}.  The abstract type @{typ
   36.13 +  satisfies the invariant \<open>is_rbt t\<close>.  The abstract type @{typ
   36.14    "('k, 'v) rbt"} always obeys this invariant, and for this reason you
   36.15    should only use this in our application.  Going back to @{typ "('k,
   36.16    'v) RBT_Impl.rbt"} may be necessary in proofs if not yet proven
   36.17 @@ -155,25 +155,25 @@
   36.18  
   36.19  text \<open>
   36.20    \noindent
   36.21 -  @{thm Empty_is_rbt}\hfill(@{text "Empty_is_rbt"})
   36.22 +  @{thm Empty_is_rbt}\hfill(\<open>Empty_is_rbt\<close>)
   36.23  
   36.24    \noindent
   36.25 -  @{thm rbt_insert_is_rbt}\hfill(@{text "rbt_insert_is_rbt"})
   36.26 +  @{thm rbt_insert_is_rbt}\hfill(\<open>rbt_insert_is_rbt\<close>)
   36.27  
   36.28    \noindent
   36.29 -  @{thm rbt_delete_is_rbt}\hfill(@{text "delete_is_rbt"})
   36.30 +  @{thm rbt_delete_is_rbt}\hfill(\<open>delete_is_rbt\<close>)
   36.31  
   36.32    \noindent
   36.33 -  @{thm rbt_bulkload_is_rbt}\hfill(@{text "bulkload_is_rbt"})
   36.34 +  @{thm rbt_bulkload_is_rbt}\hfill(\<open>bulkload_is_rbt\<close>)
   36.35  
   36.36    \noindent
   36.37 -  @{thm rbt_map_entry_is_rbt}\hfill(@{text "map_entry_is_rbt"})
   36.38 +  @{thm rbt_map_entry_is_rbt}\hfill(\<open>map_entry_is_rbt\<close>)
   36.39  
   36.40    \noindent
   36.41 -  @{thm map_is_rbt}\hfill(@{text "map_is_rbt"})
   36.42 +  @{thm map_is_rbt}\hfill(\<open>map_is_rbt\<close>)
   36.43  
   36.44    \noindent
   36.45 -  @{thm rbt_union_is_rbt}\hfill(@{text "union_is_rbt"})
   36.46 +  @{thm rbt_union_is_rbt}\hfill(\<open>union_is_rbt\<close>)
   36.47  \<close>
   36.48  
   36.49  
   36.50 @@ -181,27 +181,27 @@
   36.51  
   36.52  text \<open>
   36.53    \noindent
   36.54 -  \underline{@{text "lookup_empty"}}
   36.55 +  \underline{\<open>lookup_empty\<close>}
   36.56    @{thm [display] lookup_empty}
   36.57    \vspace{1ex}
   36.58  
   36.59    \noindent
   36.60 -  \underline{@{text "lookup_insert"}}
   36.61 +  \underline{\<open>lookup_insert\<close>}
   36.62    @{thm [display] lookup_insert}
   36.63    \vspace{1ex}
   36.64  
   36.65    \noindent
   36.66 -  \underline{@{text "lookup_delete"}}
   36.67 +  \underline{\<open>lookup_delete\<close>}
   36.68    @{thm [display] lookup_delete}
   36.69    \vspace{1ex}
   36.70  
   36.71    \noindent
   36.72 -  \underline{@{text "lookup_bulkload"}}
   36.73 +  \underline{\<open>lookup_bulkload\<close>}
   36.74    @{thm [display] lookup_bulkload}
   36.75    \vspace{1ex}
   36.76  
   36.77    \noindent
   36.78 -  \underline{@{text "lookup_map"}}
   36.79 +  \underline{\<open>lookup_map\<close>}
   36.80    @{thm [display] lookup_map}
   36.81    \vspace{1ex}
   36.82  \<close>
    37.1 --- a/src/HOL/Library/Ramsey.thy	Thu Nov 05 10:35:37 2015 +0100
    37.2 +++ b/src/HOL/Library/Ramsey.thy	Thu Nov 05 10:39:49 2015 +0100
    37.3 @@ -120,7 +120,7 @@
    37.4  subsubsection \<open>``Axiom'' of Dependent Choice\<close>
    37.5  
    37.6  primrec choice :: "('a => bool) => ('a * 'a) set => nat => 'a" where
    37.7 -  --\<open>An integer-indexed chain of choices\<close>
    37.8 +  \<comment>\<open>An integer-indexed chain of choices\<close>
    37.9      choice_0:   "choice P r 0 = (SOME x. P x)"
   37.10    | choice_Suc: "choice P r (Suc n) = (SOME y. P y & (choice P r n, y) \<in> r)"
   37.11  
   37.12 @@ -157,7 +157,7 @@
   37.13  subsubsection \<open>Partitions of a Set\<close>
   37.14  
   37.15  definition part :: "nat => nat => 'a set => ('a set => nat) => bool"
   37.16 -  --\<open>the function @{term f} partitions the @{term r}-subsets of the typically
   37.17 +  \<comment>\<open>the function @{term f} partitions the @{term r}-subsets of the typically
   37.18         infinite set @{term Y} into @{term s} distinct categories.\<close>
   37.19  where
   37.20    "part r s Y f = (\<forall>X. X \<subseteq> Y & finite X & card X = r --> f X < s)"
    38.1 --- a/src/HOL/Library/Set_Algebras.thy	Thu Nov 05 10:35:37 2015 +0100
    38.2 +++ b/src/HOL/Library/Set_Algebras.thy	Thu Nov 05 10:39:49 2015 +0100
    38.3 @@ -11,7 +11,7 @@
    38.4  text \<open>
    38.5    This library lifts operations like addition and multiplication to
    38.6    sets.  It was designed to support asymptotic calculations. See the
    38.7 -  comments at the top of theory @{text BigO}.
    38.8 +  comments at the top of theory \<open>BigO\<close>.
    38.9  \<close>
   38.10  
   38.11  instantiation set :: (plus) plus
    39.1 --- a/src/HOL/Library/State_Monad.thy	Thu Nov 05 10:35:37 2015 +0100
    39.2 +++ b/src/HOL/Library/State_Monad.thy	Thu Nov 05 10:39:49 2015 +0100
    39.3 @@ -32,26 +32,26 @@
    39.4  
    39.5    \begin{description}
    39.6  
    39.7 -    \item[transformations] with type signature @{text "\<sigma> \<Rightarrow> \<sigma>'"},
    39.8 +    \item[transformations] with type signature \<open>\<sigma> \<Rightarrow> \<sigma>'\<close>,
    39.9        transforming a state.
   39.10  
   39.11 -    \item[``yielding'' transformations] with type signature @{text "\<sigma>
   39.12 -      \<Rightarrow> \<alpha> \<times> \<sigma>'"}, ``yielding'' a side result while transforming a
   39.13 +    \item[``yielding'' transformations] with type signature \<open>\<sigma>
   39.14 +      \<Rightarrow> \<alpha> \<times> \<sigma>'\<close>, ``yielding'' a side result while transforming a
   39.15        state.
   39.16  
   39.17 -    \item[queries] with type signature @{text "\<sigma> \<Rightarrow> \<alpha>"}, computing a
   39.18 +    \item[queries] with type signature \<open>\<sigma> \<Rightarrow> \<alpha>\<close>, computing a
   39.19        result dependent on a state.
   39.20  
   39.21    \end{description}
   39.22  
   39.23 -  By convention we write @{text "\<sigma>"} for types representing states and
   39.24 -  @{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"} for types
   39.25 +  By convention we write \<open>\<sigma>\<close> for types representing states and
   39.26 +  \<open>\<alpha>\<close>, \<open>\<beta>\<close>, \<open>\<gamma>\<close>, \<open>\<dots>\<close> for types
   39.27    representing side results.  Type changes due to transformations are
   39.28    not excluded in our scenario.
   39.29  
   39.30 -  We aim to assert that values of any state type @{text "\<sigma>"} are used
   39.31 +  We aim to assert that values of any state type \<open>\<sigma>\<close> are used
   39.32    in a single-threaded way: after application of a transformation on a
   39.33 -  value of type @{text "\<sigma>"}, the former value should not be used
   39.34 +  value of type \<open>\<sigma>\<close>, the former value should not be used
   39.35    again.  To achieve this, we use a set of monad combinators:
   39.36  \<close>
   39.37  
    40.1 --- a/src/HOL/Library/Sublist_Order.thy	Thu Nov 05 10:35:37 2015 +0100
    40.2 +++ b/src/HOL/Library/Sublist_Order.thy	Thu Nov 05 10:39:49 2015 +0100
    40.3 @@ -11,8 +11,8 @@
    40.4  
    40.5  text \<open>
    40.6    This theory defines sublist ordering on lists.
    40.7 -  A list @{text ys} is a sublist of a list @{text xs},
    40.8 -  iff one obtains @{text ys} by erasing some elements from @{text xs}.
    40.9 +  A list \<open>ys\<close> is a sublist of a list \<open>xs\<close>,
   40.10 +  iff one obtains \<open>ys\<close> by erasing some elements from \<open>xs\<close>.
   40.11  \<close>
   40.12  
   40.13  subsection \<open>Definitions and basic lemmas\<close>
    41.1 --- a/src/HOL/Library/Tree.thy	Thu Nov 05 10:35:37 2015 +0100
    41.2 +++ b/src/HOL/Library/Tree.thy	Thu Nov 05 10:39:49 2015 +0100
    41.3 @@ -146,7 +146,7 @@
    41.4    (heap l \<and> heap r \<and> (\<forall>x \<in> set_tree l \<union> set_tree r. m \<le> x))"
    41.5  
    41.6  
    41.7 -subsection "Function @{text mirror}"
    41.8 +subsection "Function \<open>mirror\<close>"
    41.9  
   41.10  fun mirror :: "'a tree \<Rightarrow> 'a tree" where
   41.11  "mirror \<langle>\<rangle> = Leaf" |