--- 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
--- 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>
--- 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])"
--- 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 "<="
--- 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 =
--- 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>
--- 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)"
--- 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)
--- 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)
--- 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
--- 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)
--- 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
--- 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
--- 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 *)
--- 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)
--- 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)
--- 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:
--- 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"
--- 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"
--- 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>
--- 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)"
--- 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
--- 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)
--- 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 .
--- 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
--- 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>
--- 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"
--- 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>
--- 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
--- 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>
--- 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
--- 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"
--- 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
--- 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}"
--- 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)"
--- 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>
--- 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)"
--- 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
--- 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>
--- 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>
--- 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" |