--- a/src/Doc/Classes/Classes.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Classes/Classes.thy Sun Jan 15 18:30:18 2023 +0100
@@ -5,7 +5,7 @@
section \<open>Introduction\<close>
text \<open>
- Type classes were introduced by Wadler and Blott @{cite wadler89how}
+ Type classes were introduced by Wadler and Blott \<^cite>\<open>wadler89how\<close>
into the Haskell language to allow for a reasonable implementation
of overloading\footnote{throughout this tutorial, we are referring
to classical Haskell 1.0 type classes, not considering later
@@ -43,7 +43,7 @@
Indeed, type classes not only allow for simple overloading but form
a generic calculus, an instance of order-sorted algebra
- @{cite "nipkow-sorts93" and "Nipkow-Prehofer:1993" and "Wenzel:1997:TPHOL"}.
+ \<^cite>\<open>"nipkow-sorts93" and "Nipkow-Prehofer:1993" and "Wenzel:1997:TPHOL"\<close>.
From a software engineering point of view, type classes roughly
correspond to interfaces in object-oriented languages like Java; so,
@@ -67,7 +67,7 @@
\<^noindent> From a theoretical point of view, type classes are
lightweight modules; Haskell type classes may be emulated by SML
- functors @{cite classes_modules}. Isabelle/Isar offers a discipline
+ functors \<^cite>\<open>classes_modules\<close>. Isabelle/Isar offers a discipline
of type classes which brings all those aspects together:
\begin{enumerate}
@@ -77,17 +77,17 @@
type
\item in connection with a ``less ad-hoc'' approach to overloading,
\item with a direct link to the Isabelle module system:
- locales @{cite "kammueller-locales"}.
+ locales \<^cite>\<open>"kammueller-locales"\<close>.
\end{enumerate}
\<^noindent> Isar type classes also directly support code generation in
a Haskell like fashion. Internally, they are mapped to more
- primitive Isabelle concepts @{cite "Haftmann-Wenzel:2006:classes"}.
+ primitive Isabelle concepts \<^cite>\<open>"Haftmann-Wenzel:2006:classes"\<close>.
This tutorial demonstrates common elements of structured
specifications and abstract reasoning with type classes by the
algebraic hierarchy of semigroups, monoids and groups. Our
- background theory is that of Isabelle/HOL @{cite "isa-tutorial"}, for
+ background theory is that of Isabelle/HOL \<^cite>\<open>"isa-tutorial"\<close>, for
which some familiarity is assumed.
\<close>
@@ -418,7 +418,7 @@
\<^noindent> As you can see from this example, for local definitions
you may use any specification tool which works together with
locales, such as Krauss's recursive function package
- @{cite krauss2006}.
+ \<^cite>\<open>krauss2006\<close>.
\<close>
@@ -576,7 +576,7 @@
overloading, it is obvious that overloading stemming from @{command
class} statements and @{command instantiation} targets naturally
maps to Haskell type classes. The code generator framework
- @{cite "isabelle-codegen"} takes this into account. If the target
+ \<^cite>\<open>"isabelle-codegen"\<close> takes this into account. If the target
language (e.g.~SML) lacks type classes, then they are implemented by
an explicit dictionary construction. As example, let's go back to
the power function:
--- a/src/Doc/Codegen/Computations.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Codegen/Computations.thy Sun Jan 15 18:30:18 2023 +0100
@@ -263,7 +263,7 @@
text \<open>
Computations are a device to implement fast proof procedures.
Then results of a computation are often assumed to be trustable
- and thus wrapped in oracles (see @{cite "isabelle-isar-ref"}),
+ and thus wrapped in oracles (see \<^cite>\<open>"isabelle-isar-ref"\<close>),
as in the following example:\footnote{
The technical details how numerals are dealt with are given later in
\secref{sec:literal_input}.}
@@ -295,7 +295,7 @@
text \<open>
\<^item> Antiquotation @{ML_antiquotation computation_conv} basically yields
a conversion of type \<^ML_type>\<open>Proof.context -> cterm -> thm\<close>
- (see further @{cite "isabelle-implementation"}).
+ (see further \<^cite>\<open>"isabelle-implementation"\<close>).
\<^item> The antiquotation expects one functional argument to bridge the
\qt{untrusted gap}; this can be done e.g.~using an oracle. Since that oracle
--- a/src/Doc/Codegen/Evaluation.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Codegen/Evaluation.thy Sun Jan 15 18:30:18 2023 +0100
@@ -57,7 +57,7 @@
subsubsection \<open>Normalization by evaluation (\<open>nbe\<close>)\<close>
text \<open>
- Normalization by evaluation @{cite "Aehlig-Haftmann-Nipkow:2008:nbe"}
+ Normalization by evaluation \<^cite>\<open>"Aehlig-Haftmann-Nipkow:2008:nbe"\<close>
provides a comparably fast partially symbolic evaluation which
permits also normalization of functions and uninterpreted symbols;
the stack of code to be trusted is considerable.
--- a/src/Doc/Codegen/Further.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Codegen/Further.thy Sun Jan 15 18:30:18 2023 +0100
@@ -174,7 +174,7 @@
can be generated. But this not the case: internally, the term
\<open>fun_power.powers\<close> is an abbreviation for the foundational
term @{term [source] "power.powers (\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"}
- (see @{cite "isabelle-locale"} for the details behind).
+ (see \<^cite>\<open>"isabelle-locale"\<close> for the details behind).
Fortunately, a succint solution is available: a dedicated
rewrite definition:
@@ -212,7 +212,7 @@
If you consider imperative data structures as inevitable for a
specific application, you should consider \emph{Imperative
Functional Programming with Isabelle/HOL}
- @{cite "bulwahn-et-al:2008:imperative"}; the framework described there
+ \<^cite>\<open>"bulwahn-et-al:2008:imperative"\<close>; the framework described there
is available in session \<open>Imperative_HOL\<close>, together with a
short primer document.
\<close>
--- a/src/Doc/Codegen/Inductive_Predicate.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Codegen/Inductive_Predicate.thy Sun Jan 15 18:30:18 2023 +0100
@@ -23,7 +23,7 @@
which turns inductive specifications into equational ones, from
which in turn executable code can be generated. The mechanisms of
this compiler are described in detail in
- @{cite "Berghofer-Bulwahn-Haftmann:2009:TPHOL"}.
+ \<^cite>\<open>"Berghofer-Bulwahn-Haftmann:2009:TPHOL"\<close>.
Consider the simple predicate \<^const>\<open>append\<close> given by these two
introduction rules:
--- a/src/Doc/Codegen/Introduction.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Codegen/Introduction.thy Sun Jan 15 18:30:18 2023 +0100
@@ -11,12 +11,12 @@
text \<open>
This tutorial introduces the code generator facilities of \<open>Isabelle/HOL\<close>. It allows to turn (a certain class of) HOL
specifications into corresponding executable code in the programming
- languages \<open>SML\<close> @{cite SML}, \<open>OCaml\<close> @{cite OCaml},
- \<open>Haskell\<close> @{cite "haskell-revised-report"} and \<open>Scala\<close>
- @{cite "scala-overview-tech-report"}.
+ languages \<open>SML\<close> \<^cite>\<open>SML\<close>, \<open>OCaml\<close> \<^cite>\<open>OCaml\<close>,
+ \<open>Haskell\<close> \<^cite>\<open>"haskell-revised-report"\<close> and \<open>Scala\<close>
+ \<^cite>\<open>"scala-overview-tech-report"\<close>.
To profit from this tutorial, some familiarity and experience with
- Isabelle/HOL @{cite "isa-tutorial"} and its basic theories is assumed.
+ Isabelle/HOL \<^cite>\<open>"isa-tutorial"\<close> and its basic theories is assumed.
\<close>
@@ -31,7 +31,7 @@
a generated program as an implementation of a higher-order rewrite
system, then every rewrite step performed by the program can be
simulated in the logic, which guarantees partial correctness
- @{cite "Haftmann-Nipkow:2010:code"}.
+ \<^cite>\<open>"Haftmann-Nipkow:2010:code"\<close>.
\<close>
@@ -235,11 +235,11 @@
\item You may want to skim over the more technical sections
\secref{sec:adaptation} and \secref{sec:further}.
- \item The target language Scala @{cite "scala-overview-tech-report"}
+ \item The target language Scala \<^cite>\<open>"scala-overview-tech-report"\<close>
comes with some specialities discussed in \secref{sec:scala}.
\item For exhaustive syntax diagrams etc. you should visit the
- Isabelle/Isar Reference Manual @{cite "isabelle-isar-ref"}.
+ Isabelle/Isar Reference Manual \<^cite>\<open>"isabelle-isar-ref"\<close>.
\end{itemize}
--- a/src/Doc/Codegen/Partial_Functions.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Codegen/Partial_Functions.thy Sun Jan 15 18:30:18 2023 +0100
@@ -130,7 +130,7 @@
Type \<open>dlist\<close> in Section~\ref{sec:partiality} is defined in the same manner.
The following command sets up infrastructure for lifting functions on @{typ "nat list"}
-to @{typ acyc} (used by @{command_def lift_definition} below) \cite{isabelle-isar-ref}.\<close>
+to @{typ acyc} (used by @{command_def lift_definition} below) \<^cite>\<open>"isabelle-isar-ref"\<close>.\<close>
setup_lifting type_definition_acyc
--- a/src/Doc/Codegen/Refinement.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Codegen/Refinement.thy Sun Jan 15 18:30:18 2023 +0100
@@ -265,7 +265,7 @@
\<close>
text \<open>
- See further @{cite "Haftmann-Kraus-Kuncar-Nipkow:2013:data_refinement"}
+ See further \<^cite>\<open>"Haftmann-Kraus-Kuncar-Nipkow:2013:data_refinement"\<close>
for the meta theory of datatype refinement involving invariants.
Typical data structures implemented by representations involving
--- a/src/Doc/Corec/Corec.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Corec/Corec.thy Sun Jan 15 18:30:18 2023 +0100
@@ -17,7 +17,7 @@
\label{sec:introduction}\<close>
text \<open>
-Isabelle's (co)datatype package @{cite "isabelle-datatypes"} offers a convenient
+Isabelle's (co)datatype package \<^cite>\<open>"isabelle-datatypes"\<close> offers a convenient
syntax for introducing codatatypes. For example, the type of (infinite) streams
can be defined as follows (cf. \<^file>\<open>~~/src/HOL/Library/Stream.thy\<close>):
\<close>
@@ -70,13 +70,13 @@
terminology, corecursion and coinduction take place \emph{up to} friendly
contexts.
-The package fully adheres to the LCF philosophy @{cite mgordon79}: The
+The package fully adheres to the LCF philosophy \<^cite>\<open>mgordon79\<close>: The
characteristic theorems associated with the specified corecursive functions are
derived rather than introduced axiomatically.
(Exceptionally, most of the internal proof obligations are omitted if the
\<open>quick_and_dirty\<close> option is enabled.)
The package is described in a pair of scientific papers
-@{cite "blanchette-et-al-2015-fouco" and "blanchette-et-al-201x-amico"}. Some
+\<^cite>\<open>"blanchette-et-al-2015-fouco" and "blanchette-et-al-201x-amico"\<close>. Some
of the text and examples below originate from there.
This tutorial is organized as follows:
@@ -137,7 +137,7 @@
\label{ssec:simple-corecursion}\<close>
text \<open>
-The case studies by Rutten~@{cite rutten05} and Hinze~@{cite hinze10} on stream
+The case studies by Rutten~\<^cite>\<open>rutten05\<close> and Hinze~\<^cite>\<open>hinze10\<close> on stream
calculi serve as our starting point. The following definition of pointwise sum
can be performed with either \keyw{primcorec} or @{command corec}:
\<close>
@@ -229,7 +229,7 @@
text \<open>
\noindent
In general, the arguments may be any bounded natural functor (BNF)
-@{cite "isabelle-datatypes"}, with the restriction that the target codatatype
+\<^cite>\<open>"isabelle-datatypes"\<close>, with the restriction that the target codatatype
(\<^typ>\<open>nat stream\<close>) may occur only in a \emph{live} position of the BNF. For
this reason, the following function, on unbounded sets, cannot be registered as
a friend:
@@ -323,7 +323,7 @@
reaching a guarded corecursive call. Intuitively, the unguarded recursive call
can be unfolded to arbitrary finite depth, ultimately yielding a purely
corecursive definition. An example is the \<^term>\<open>primes\<close> function from Di
-Gianantonio and Miculan @{cite "di-gianantonio-miculan-2003"}:
+Gianantonio and Miculan \<^cite>\<open>"di-gianantonio-miculan-2003"\<close>:
\<close>
corecursive primes :: "nat \<Rightarrow> nat \<Rightarrow> nat stream" where
@@ -356,7 +356,7 @@
There is a slight complication when \<open>m = 0 \<and> n > 1\<close>: Without the first
disjunct in the \<open>if\<close> condition, the function could stall. (This corner
case was overlooked in the original example
-@{cite "di-gianantonio-miculan-2003"}.)
+\<^cite>\<open>"di-gianantonio-miculan-2003"\<close>.)
In the following examples, termination is discharged automatically by
@{command corec} by invoking @{method lexicographic_order}:
@@ -640,7 +640,7 @@
The syntactic entity \synt{target} can be used to specify a local context,
\synt{fix} denotes name with an optional type signature, and \synt{prop} denotes
-a HOL proposition @{cite "isabelle-isar-ref"}.
+a HOL proposition \<^cite>\<open>"isabelle-isar-ref"\<close>.
The optional target is optionally followed by a combination of the following
options:
@@ -692,7 +692,7 @@
The syntactic entity \synt{target} can be used to specify a local context,
\synt{fix} denotes name with an optional type signature, and \synt{prop} denotes
-a HOL proposition @{cite "isabelle-isar-ref"}.
+a HOL proposition \<^cite>\<open>"isabelle-isar-ref"\<close>.
The optional target is optionally followed by a combination of the following
options:
@@ -732,7 +732,7 @@
specified prefix.
The syntactic entity \synt{name} denotes an identifier and \synt{type} denotes a
-type @{cite "isabelle-isar-ref"}.
+type \<^cite>\<open>"isabelle-isar-ref"\<close>.
\<close>
@@ -784,7 +784,7 @@
\item[\<open>f.\<close>\hthm{code} \<open>[code]\<close>\rm:] ~ \\
@{thm sexp.code[no_vars]} \\
The \<open>[code]\<close> attribute is set by the \<open>code\<close> plugin
-@{cite "isabelle-datatypes"}.
+\<^cite>\<open>"isabelle-datatypes"\<close>.
\item[\<open>f.\<close>\hthm{coinduct} \<open>[consumes 1, case_names t, case_conclusion D\<^sub>1 \<dots>
D\<^sub>n]\<close>\rm:] ~ \\
--- a/src/Doc/Datatypes/Datatypes.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Sun Jan 15 18:30:18 2023 +0100
@@ -29,7 +29,7 @@
text \<open>
The 2013 edition of Isabelle introduced a definitional package for freely
generated datatypes and codatatypes. This package replaces the earlier
-implementation due to Berghofer and Wenzel @{cite "Berghofer-Wenzel:1999:TPHOL"}.
+implementation due to Berghofer and Wenzel \<^cite>\<open>"Berghofer-Wenzel:1999:TPHOL"\<close>.
Perhaps the main advantage of the new package is that it supports recursion
through a large class of non-datatypes, such as finite sets:
\<close>
@@ -85,14 +85,14 @@
the theory \<^file>\<open>~~/src/HOL/Library/BNF_Axiomatization.thy\<close>.
The package, like its predecessor, fully adheres to the LCF philosophy
-@{cite mgordon79}: The characteristic theorems associated with the specified
+\<^cite>\<open>mgordon79\<close>: The characteristic theorems associated with the specified
(co)datatypes are derived rather than introduced axiomatically.%
\footnote{However, some of the
internal constructions and most of the internal proof obligations are omitted
if the \<open>quick_and_dirty\<close> option is enabled.}
The package is described in a number of scientific papers
-@{cite "traytel-et-al-2012" and "blanchette-et-al-2014-impl" and
-"panny-et-al-2014" and "blanchette-et-al-2015-wit"}.
+\<^cite>\<open>"traytel-et-al-2012" and "blanchette-et-al-2014-impl" and
+"panny-et-al-2014" and "blanchette-et-al-2015-wit"\<close>.
The central notion is that of a \emph{bounded natural functor} (BNF)---a
well-behaved type constructor for which nested (co)recursion is supported.
@@ -106,7 +106,7 @@
\item Section \ref{sec:defining-primitively-recursive-functions}, ``Defining
Primitively Recursive Functions,'' describes how to specify functions
-using @{command primrec}. (A separate tutorial @{cite "isabelle-function"}
+using @{command primrec}. (A separate tutorial \<^cite>\<open>"isabelle-function"\<close>
describes the more powerful \keyw{fun} and \keyw{function} commands.)
\item Section \ref{sec:defining-codatatypes}, ``Defining Codatatypes,''
@@ -116,7 +116,7 @@
``Defining Primitively Corecursive Functions,'' describes how to specify
functions using the @{command primcorec} and
@{command primcorecursive} commands. (A separate tutorial
-@{cite "isabelle-corec"} describes the more powerful \keyw{corec} and
+\<^cite>\<open>"isabelle-corec"\<close> describes the more powerful \keyw{corec} and
\keyw{corecursive} commands.)
\item Section \ref{sec:registering-bounded-natural-functors}, ``Registering
@@ -493,7 +493,7 @@
datatypes specified by their constructors.
The syntactic entity \synt{target} can be used to specify a local
-context (e.g., \<open>(in linorder)\<close> @{cite "isabelle-isar-ref"}),
+context (e.g., \<open>(in linorder)\<close> \<^cite>\<open>"isabelle-isar-ref"\<close>),
and \synt{prop} denotes a HOL proposition.
The optional target is optionally followed by a combination of the following
@@ -531,7 +531,7 @@
\noindent
The syntactic entity \synt{name} denotes an identifier, \synt{mixfix} denotes
the usual parenthesized mixfix notation, and \synt{typefree} denotes fixed type
-variable (\<^typ>\<open>'a\<close>, \<^typ>\<open>'b\<close>, \ldots) @{cite "isabelle-isar-ref"}.
+variable (\<^typ>\<open>'a\<close>, \<^typ>\<open>'b\<close>, \ldots) \<^cite>\<open>"isabelle-isar-ref"\<close>.
The optional names preceding the type variables allow to override the default
names of the set functions (\<open>set\<^sub>1_t\<close>, \ldots, \<open>set\<^sub>m_t\<close>). Type
@@ -566,7 +566,7 @@
\medskip
\noindent
-The syntactic entity \synt{type} denotes a HOL type @{cite "isabelle-isar-ref"}.
+The syntactic entity \synt{type} denotes a HOL type \<^cite>\<open>"isabelle-isar-ref"\<close>.
In addition to the type of a constructor argument, it is possible to specify a
name for the corresponding selector. The same selector name can be reused for
@@ -602,7 +602,7 @@
ML \<open>Old_Datatype_Data.get_info \<^theory> \<^type_name>\<open>even_nat\<close>\<close>
text \<open>
-The syntactic entity \synt{name} denotes an identifier @{cite "isabelle-isar-ref"}.
+The syntactic entity \synt{name} denotes an identifier \<^cite>\<open>"isabelle-isar-ref"\<close>.
The command is sometimes useful when migrating from the old datatype package to
the new one.
@@ -1256,7 +1256,7 @@
command, which supports primitive recursion, or using the \keyw{fun},
\keyw{function}, and \keyw{partial_function} commands. In this tutorial, the
focus is on @{command primrec}; \keyw{fun} and \keyw{function} are described in
-a separate tutorial @{cite "isabelle-function"}.
+a separate tutorial \<^cite>\<open>"isabelle-function"\<close>.
Because it is restricted to primitive recursion, @{command primrec} is less
powerful than \keyw{fun} and \keyw{function}. However, there are primitively
@@ -1616,7 +1616,7 @@
The syntactic entity \synt{target} can be used to specify a local context,
\synt{fixes} denotes a list of names with optional type signatures,
\synt{thmdecl} denotes an optional name for the formula that follows, and
-\synt{prop} denotes a HOL proposition @{cite "isabelle-isar-ref"}.
+\synt{prop} denotes a HOL proposition \<^cite>\<open>"isabelle-isar-ref"\<close>.
The optional target is optionally followed by a combination of the following
options:
@@ -1787,8 +1787,7 @@
command is first illustrated through concrete examples featuring different
flavors of corecursion. More examples can be found in the directory
\<^dir>\<open>~~/src/HOL/Datatype_Examples\<close>. The \emph{Archive of Formal Proofs} also
-includes some useful codatatypes, notably for lazy lists @{cite
-"lochbihler-2010"}.
+includes some useful codatatypes, notably for lazy lists \<^cite>\<open>"lochbihler-2010"\<close>.
\<close>
@@ -2080,10 +2079,10 @@
\keyw{prim\-corec\-ursive} commands, which support primitive corecursion.
Other approaches include the more general \keyw{partial_function} command, the
\keyw{corec} and \keyw{corecursive} commands, and techniques based on domains
-and topologies @{cite "lochbihler-hoelzl-2014"}. In this tutorial, the focus is
+and topologies \<^cite>\<open>"lochbihler-hoelzl-2014"\<close>. In this tutorial, the focus is
on @{command primcorec} and @{command primcorecursive}; \keyw{corec} and
\keyw{corecursive} are described in a separate tutorial
-@{cite "isabelle-corec"}. More examples can be found in the directories
+\<^cite>\<open>"isabelle-corec"\<close>. More examples can be found in the directories
\<^dir>\<open>~~/src/HOL/Datatype_Examples\<close> and \<^dir>\<open>~~/src/HOL/Corec_Examples\<close>.
Whereas recursive functions consume datatypes one constructor at a time,
@@ -2624,7 +2623,7 @@
The syntactic entity \synt{target} can be used to specify a local context,
\synt{fixes} denotes a list of names with optional type signatures,
\synt{thmdecl} denotes an optional name for the formula that follows, and
-\synt{prop} denotes a HOL proposition @{cite "isabelle-isar-ref"}.
+\synt{prop} denotes a HOL proposition \<^cite>\<open>"isabelle-isar-ref"\<close>.
The optional target is optionally followed by a combination of the following
options:
@@ -2785,7 +2784,7 @@
text \<open>
Bounded natural functors (BNFs) are a semantic criterion for where
(co)re\-cur\-sion may appear on the right-hand side of an equation
-@{cite "traytel-et-al-2012" and "blanchette-et-al-2015-wit"}.
+\<^cite>\<open>"traytel-et-al-2012" and "blanchette-et-al-2015-wit"\<close>.
An $n$-ary BNF is a type constructor equipped with a map function
(functorial action), $n$ set functions (natural transformations),
@@ -3105,7 +3104,7 @@
The syntactic entity \synt{target} can be used to specify a local context,
\synt{type} denotes a HOL type, and \synt{term} denotes a HOL term
-@{cite "isabelle-isar-ref"}.
+\<^cite>\<open>"isabelle-isar-ref"\<close>.
The @{syntax plugins} option indicates which plugins should be enabled
(\<open>only\<close>) or disabled (\<open>del\<close>). By default, all plugins are enabled.
@@ -3203,7 +3202,7 @@
\synt{name} denotes an identifier, \synt{typefree} denotes fixed type variable
(\<^typ>\<open>'a\<close>, \<^typ>\<open>'b\<close>, \ldots), \synt{mixfix} denotes the usual parenthesized
mixfix notation, and \synt{types} denotes a space-separated list of types
-@{cite "isabelle-isar-ref"}.
+\<^cite>\<open>"isabelle-isar-ref"\<close>.
The @{syntax plugins} option indicates which plugins should be enabled
(\<open>only\<close>) or disabled (\<open>del\<close>). By default, all plugins are enabled.
@@ -3288,7 +3287,7 @@
The syntactic entity \synt{target} can be used to specify a local context,
\synt{name} denotes an identifier, \synt{prop} denotes a HOL proposition, and
-\synt{term} denotes a HOL term @{cite "isabelle-isar-ref"}.
+\synt{term} denotes a HOL term \<^cite>\<open>"isabelle-isar-ref"\<close>.
The syntax resembles that of @{command datatype} and @{command codatatype}
definitions (Sections
@@ -3410,7 +3409,7 @@
text \<open>
Beyond the standard plugins, the \emph{Archive of Formal Proofs} includes a
\keyw{derive} command that derives class instances of datatypes
-@{cite "sternagel-thiemann-2015"}.
+\<^cite>\<open>"sternagel-thiemann-2015"\<close>.
\<close>
subsection \<open>Code Generator
--- a/src/Doc/Demo_EPTCS/Document.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Demo_EPTCS/Document.thy Sun Jan 15 18:30:18 2023 +0100
@@ -23,7 +23,7 @@
paragraph \<open>Another paragraph.\<close>
-text \<open>See also @{cite \<open>\S3\<close> "isabelle-system"}.\<close>
+text \<open>See also \<^cite>\<open>\<open>\S3\<close> in "isabelle-system"\<close>.\<close>
section \<open>Formal proof of Cantor's theorem\<close>
--- a/src/Doc/Demo_Easychair/Document.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Demo_Easychair/Document.thy Sun Jan 15 18:30:18 2023 +0100
@@ -23,7 +23,7 @@
paragraph \<open>Another paragraph.\<close>
-text \<open>See also @{cite \<open>\S3\<close> "isabelle-system"}.\<close>
+text \<open>See also \<^cite>\<open>\<open>\S3\<close> in "isabelle-system"\<close>.\<close>
section \<open>Formal proof of Cantor's theorem\<close>
--- a/src/Doc/Demo_LIPIcs/Document.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Demo_LIPIcs/Document.thy Sun Jan 15 18:30:18 2023 +0100
@@ -23,7 +23,7 @@
paragraph \<open>Another paragraph.\<close>
-text \<open>See also @{cite \<open>\S3\<close> "isabelle-system"}.\<close>
+text \<open>See also \<^cite>\<open>\<open>\S3\<close> in "isabelle-system"\<close>.\<close>
section \<open>Formal proof of Cantor's theorem\<close>
--- a/src/Doc/Demo_LLNCS/Document.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Demo_LLNCS/Document.thy Sun Jan 15 18:30:18 2023 +0100
@@ -23,7 +23,7 @@
paragraph \<open>Another paragraph.\<close>
-text \<open>See also @{cite \<open>\S3\<close> "isabelle-system"}.\<close>
+text \<open>See also \<^cite>\<open>\<open>\S3\<close> in "isabelle-system"\<close>.\<close>
section \<open>Formal proof of Cantor's theorem\<close>
--- a/src/Doc/Eisbach/Manual.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Eisbach/Manual.thy Sun Jan 15 18:30:18 2023 +0100
@@ -15,7 +15,7 @@
\<^medskip>
The syntax diagram below refers to some syntactic categories that are
- further defined in @{cite "isabelle-isar-ref"}.
+ further defined in \<^cite>\<open>"isabelle-isar-ref"\<close>.
\<^rail>\<open>
@@{command method} name args @'=' method
@@ -281,7 +281,7 @@
\<^medskip>
The syntax diagram below refers to some syntactic categories that are
- further defined in @{cite "isabelle-isar-ref"}.
+ further defined in \<^cite>\<open>"isabelle-isar-ref"\<close>.
\<^rail>\<open>
@@{method match} kind @'in' (pattern '\<Rightarrow>' @{syntax text} + '\<bar>')
--- a/src/Doc/Eisbach/Preface.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Eisbach/Preface.thy Sun Jan 15 18:30:18 2023 +0100
@@ -6,7 +6,7 @@
text \<open>
\<^emph>\<open>Eisbach\<close> is a collection of tools which form the basis for defining new
- proof methods in Isabelle/Isar~@{cite "Wenzel-PhD"}. It can be thought of as
+ proof methods in Isabelle/Isar~\<^cite>\<open>"Wenzel-PhD"\<close>. It can be thought of as
a ``proof method language'', but is more precisely an infrastructure for
defining new proof methods out of existing ones.
--- a/src/Doc/Functions/Functions.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Functions/Functions.thy Sun Jan 15 18:30:18 2023 +0100
@@ -276,7 +276,7 @@
text \<open>
To see how the automatic termination proofs work, let's look at an
example where it fails\footnote{For a detailed discussion of the
- termination prover, see @{cite bulwahnKN07}}:
+ termination prover, see \<^cite>\<open>bulwahnKN07\<close>}:
\end{isamarkuptext}
\cmd{fun} \<open>fails :: "nat \<Rightarrow> nat list \<Rightarrow> nat"\<close>\\%
@@ -332,7 +332,7 @@
more powerful \<open>size_change\<close> method, which uses a variant of
the size-change principle, together with some other
techniques. While the details are discussed
- elsewhere @{cite krauss_phd},
+ elsewhere \<^cite>\<open>krauss_phd\<close>,
here are a few typical situations where
\<open>lexicographic_order\<close> has difficulties and \<open>size_change\<close>
may be worth a try:
--- a/src/Doc/Implementation/Eq.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Implementation/Eq.thy Sun Jan 15 18:30:18 2023 +0100
@@ -74,10 +74,10 @@
section \<open>Conversions \label{sec:conv}\<close>
text \<open>
- The classic article @{cite "paulson:1983"} introduces the concept of
+ The classic article \<^cite>\<open>"paulson:1983"\<close> introduces the concept of
conversion for Cambridge LCF. This was historically important to implement
all kinds of ``simplifiers'', but the Isabelle Simplifier is done quite
- differently, see @{cite \<open>\S9.3\<close> "isabelle-isar-ref"}.
+ differently, see \<^cite>\<open>\<open>\S9.3\<close> in "isabelle-isar-ref"\<close>.
\<close>
text %mlref \<open>
--- a/src/Doc/Implementation/Integration.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Implementation/Integration.thy Sun Jan 15 18:30:18 2023 +0100
@@ -15,8 +15,8 @@
stateless manner. Historically, the sequence of transitions was wrapped up
as sequential command loop, such that commands are applied one-by-one. In
contemporary Isabelle/Isar, processing toplevel commands usually works in
- parallel in multi-threaded Isabelle/ML @{cite "Wenzel:2009" and
- "Wenzel:2013:ITP"}.
+ parallel in multi-threaded Isabelle/ML \<^cite>\<open>"Wenzel:2009" and
+ "Wenzel:2013:ITP"\<close>.
\<close>
--- a/src/Doc/Implementation/Isar.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Implementation/Isar.thy Sun Jan 15 18:30:18 2023 +0100
@@ -7,7 +7,7 @@
chapter \<open>Isar language elements\<close>
text \<open>
- The Isar proof language (see also @{cite \<open>\S2\<close> "isabelle-isar-ref"})
+ The Isar proof language (see also \<^cite>\<open>\<open>\S2\<close> in "isabelle-isar-ref"\<close>)
consists of three main categories of language elements:
\<^enum> Proof \<^emph>\<open>commands\<close> define the primary language of transactions of the
@@ -86,7 +86,7 @@
\<^descr> \<^ML>\<open>Proof.assert_forward\<close>, \<^ML>\<open>Proof.assert_chain\<close>, \<^ML>\<open>Proof.assert_backward\<close> are partial identity functions that fail unless a
certain linguistic mode is active, namely ``\<open>proof(state)\<close>'',
``\<open>proof(chain)\<close>'', ``\<open>proof(prove)\<close>'', respectively (using the terminology
- of @{cite "isabelle-isar-ref"}).
+ of \<^cite>\<open>"isabelle-isar-ref"\<close>).
It is advisable study the implementations of existing proof commands for
suitable modes to be asserted.
@@ -308,7 +308,7 @@
\<close>
text %mlex \<open>
- See also @{command method_setup} in @{cite "isabelle-isar-ref"} which
+ See also @{command method_setup} in \<^cite>\<open>"isabelle-isar-ref"\<close> which
includes some abstract examples.
\<^medskip>
@@ -358,7 +358,7 @@
The \<^ML>\<open>Attrib.thms\<close> parser produces a list of theorems from the usual Isar
syntax involving attribute expressions etc.\ (syntax category @{syntax
- thms}) @{cite "isabelle-isar-ref"}. The resulting \<^ML_text>\<open>thms\<close> are
+ thms}) \<^cite>\<open>"isabelle-isar-ref"\<close>. The resulting \<^ML_text>\<open>thms\<close> are
added to \<^ML>\<open>HOL_basic_ss\<close> which already contains the basic Simplifier
setup for HOL.
@@ -540,7 +540,7 @@
\<close>
text %mlex \<open>
- See also @{command attribute_setup} in @{cite "isabelle-isar-ref"} which
+ See also @{command attribute_setup} in \<^cite>\<open>"isabelle-isar-ref"\<close> which
includes some abstract examples.
\<close>
--- a/src/Doc/Implementation/Local_Theory.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Implementation/Local_Theory.thy Sun Jan 15 18:30:18 2023 +0100
@@ -84,8 +84,8 @@
When a definitional package is finished, the auxiliary context is reset to
the target context. The target now holds definitions for terms and theorems
that stem from the hypothetical \<open>\<DEFINE>\<close> and \<open>\<NOTE>\<close> elements,
- transformed by the particular target policy (see @{cite \<open>\S4--5\<close>
- "Haftmann-Wenzel:2009"} for details).
+ transformed by the particular target policy (see \<^cite>\<open>\<open>\S4--5\<close> in
+ "Haftmann-Wenzel:2009"\<close> for details).
\<close>
text %mlref \<open>
@@ -143,7 +143,7 @@
text \<open>
%FIXME
- See also @{cite "Chaieb-Wenzel:2007"}.
+ See also \<^cite>\<open>"Chaieb-Wenzel:2007"\<close>.
\<close>
end
--- a/src/Doc/Implementation/Logic.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Implementation/Logic.thy Sun Jan 15 18:30:18 2023 +0100
@@ -8,9 +8,9 @@
text \<open>
The logical foundations of Isabelle/Isar are that of the Pure logic, which
- has been introduced as a Natural Deduction framework in @{cite paulson700}.
+ has been introduced as a Natural Deduction framework in \<^cite>\<open>paulson700\<close>.
This is essentially the same logic as ``\<open>\<lambda>HOL\<close>'' in the more abstract
- setting of Pure Type Systems (PTS) @{cite "Barendregt-Geuvers:2001"},
+ setting of Pure Type Systems (PTS) \<^cite>\<open>"Barendregt-Geuvers:2001"\<close>,
although there are some key differences in the specific treatment of simple
types in Isabelle/Pure.
@@ -97,7 +97,7 @@
sorts \<open>(s\<^sub>1, \<dots>, s\<^sub>k)\<close> such that a type scheme \<open>(\<alpha>\<^bsub>s\<^sub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^sub>k\<^esub>)\<kappa>\<close> is of
sort \<open>s\<close>. Consequently, type unification has most general solutions (modulo
equivalence of sorts), so type-inference produces primary types as expected
- @{cite "nipkow-prehofer"}.
+ \<^cite>\<open>"nipkow-prehofer"\<close>.
\<close>
text %mlref \<open>
@@ -255,8 +255,7 @@
text \<open>
The language of terms is that of simply-typed \<open>\<lambda>\<close>-calculus with de-Bruijn
- indices for bound variables (cf.\ @{cite debruijn72} or @{cite
- "paulson-ml2"}), with the types being determined by the corresponding
+ indices for bound variables (cf.\ \<^cite>\<open>debruijn72\<close> or \<^cite>\<open>"paulson-ml2"\<close>), with the types being determined by the corresponding
binders. In contrast, free variables and constants have an explicit name and
type in each occurrence.
@@ -598,15 +597,13 @@
occur within propositions. The system provides a runtime option to record
explicit proof terms for primitive inferences, see also
\secref{sec:proof-terms}. Thus all three levels of \<open>\<lambda>\<close>-calculus become
- explicit: \<open>\<Rightarrow>\<close> for terms, and \<open>\<And>/\<Longrightarrow>\<close> for proofs (cf.\ @{cite
- "Berghofer-Nipkow:2000:TPHOL"}).
+ explicit: \<open>\<Rightarrow>\<close> for terms, and \<open>\<And>/\<Longrightarrow>\<close> for proofs (cf.\ \<^cite>\<open>"Berghofer-Nipkow:2000:TPHOL"\<close>).
Observe that locally fixed parameters (as in \<open>\<And>\<hyphen>intro\<close>) need not be recorded
in the hypotheses, because the simple syntactic types of Pure are always
inhabitable. ``Assumptions'' \<open>x :: \<tau>\<close> for type-membership are only present
as long as some \<open>x\<^sub>\<tau>\<close> occurs in the statement body.\<^footnote>\<open>This is the key
- difference to ``\<open>\<lambda>HOL\<close>'' in the PTS framework @{cite
- "Barendregt-Geuvers:2001"}, where hypotheses \<open>x : A\<close> are treated uniformly
+ difference to ``\<open>\<lambda>HOL\<close>'' in the PTS framework \<^cite>\<open>"Barendregt-Geuvers:2001"\<close>, where hypotheses \<open>x : A\<close> are treated uniformly
for propositions and types.\<close>
\<^medskip>
@@ -665,8 +662,8 @@
previously defined constants as above, or arbitrary constants \<open>d(\<alpha>\<^sub>i)\<close> for
some \<open>\<alpha>\<^sub>i\<close> projected from \<open>\<^vec>\<alpha>\<close>. Thus overloaded definitions
essentially work by primitive recursion over the syntactic structure of a
- single type argument. See also @{cite \<open>\S4.3\<close>
- "Haftmann-Wenzel:2006:classes"}.
+ single type argument. See also \<^cite>\<open>\<open>\S4.3\<close> in
+ "Haftmann-Wenzel:2006:classes"\<close>.
\<close>
text %mlref \<open>
@@ -1000,8 +997,8 @@
text \<open>
The idea of object-level rules is to model Natural Deduction inferences in
- the style of Gentzen @{cite "Gentzen:1935"}, but we allow arbitrary nesting
- similar to @{cite "Schroeder-Heister:1984"}. The most basic rule format is
+ the style of Gentzen \<^cite>\<open>"Gentzen:1935"\<close>, but we allow arbitrary nesting
+ similar to \<^cite>\<open>"Schroeder-Heister:1984"\<close>. The most basic rule format is
that of a \<^emph>\<open>Horn Clause\<close>:
\[
\infer{\<open>A\<close>}{\<open>A\<^sub>1\<close> & \<open>\<dots>\<close> & \<open>A\<^sub>n\<close>}
@@ -1022,7 +1019,7 @@
Nesting of rules means that the positions of \<open>A\<^sub>i\<close> may again hold compound
rules, not just atomic propositions. Propositions of this format are called
- \<^emph>\<open>Hereditary Harrop Formulae\<close> in the literature @{cite "Miller:1991"}. Here
+ \<^emph>\<open>Hereditary Harrop Formulae\<close> in the literature \<^cite>\<open>"Miller:1991"\<close>. Here
we give an inductive characterization as follows:
\<^medskip>
@@ -1186,7 +1183,7 @@
\<open>\<lambda>\<close>-calculus are added, which correspond to \<open>\<And>x :: \<alpha>. B x\<close> and \<open>A \<Longrightarrow> B\<close>
according to the propositions-as-types principle. The resulting 3-level
\<open>\<lambda>\<close>-calculus resembles ``\<open>\<lambda>HOL\<close>'' in the more abstract setting of Pure Type
- Systems (PTS) @{cite "Barendregt-Geuvers:2001"}, if some fine points like
+ Systems (PTS) \<^cite>\<open>"Barendregt-Geuvers:2001"\<close>, if some fine points like
schematic polymorphism and type classes are ignored.
\<^medskip>
@@ -1243,8 +1240,8 @@
abstractions, and some argument terms of applications \<open>p \<cdot> t\<close> (if possible).
There are separate operations to reconstruct the full proof term later on,
- using \<^emph>\<open>higher-order pattern unification\<close> @{cite "nipkow-patterns" and
- "Berghofer-Nipkow:2000:TPHOL"}.
+ using \<^emph>\<open>higher-order pattern unification\<close> \<^cite>\<open>"nipkow-patterns" and
+ "Berghofer-Nipkow:2000:TPHOL"\<close>.
The \<^emph>\<open>proof checker\<close> expects a fully reconstructed proof term, and can turn
it into a theorem by replaying its primitive inferences within the kernel.
@@ -1255,7 +1252,7 @@
text \<open>
The concrete syntax of proof terms is a slight extension of the regular
- inner syntax of Isabelle/Pure @{cite "isabelle-isar-ref"}. Its main
+ inner syntax of Isabelle/Pure \<^cite>\<open>"isabelle-isar-ref"\<close>. Its main
syntactic category @{syntax (inner) proof} is defined as follows:
\begin{center}
--- a/src/Doc/Implementation/ML.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Implementation/ML.thy Sun Jan 15 18:30:18 2023 +0100
@@ -658,7 +658,7 @@
\<close>
Here @{syntax name} and @{syntax args} are outer syntax categories, as
- defined in @{cite "isabelle-isar-ref"}.
+ defined in \<^cite>\<open>"isabelle-isar-ref"\<close>.
\<^medskip>
A regular antiquotation \<open>@{name args}\<close> processes its arguments by the usual
@@ -966,8 +966,7 @@
different text styles or colours. The standard output for batch sessions
prefixes each line of warnings by \<^verbatim>\<open>###\<close> and errors by \<^verbatim>\<open>***\<close>, but leaves
anything else unchanged. The message body may contain further markup and
- formatting, which is routinely used in the Prover IDE @{cite
- "isabelle-jedit"}.
+ formatting, which is routinely used in the Prover IDE \<^cite>\<open>"isabelle-jedit"\<close>.
Messages are associated with the transaction context of the running Isar
command. This enables the front-end to manage commands and resulting
@@ -1316,8 +1315,7 @@
\<^descr> \<^ML>\<open>Symbol.is_letter\<close>, \<^ML>\<open>Symbol.is_digit\<close>,
\<^ML>\<open>Symbol.is_quasi\<close>, \<^ML>\<open>Symbol.is_blank\<close> classify standard symbols
- according to fixed syntactic conventions of Isabelle, cf.\ @{cite
- "isabelle-isar-ref"}.
+ according to fixed syntactic conventions of Isabelle, cf.\ \<^cite>\<open>"isabelle-isar-ref"\<close>.
\<^descr> Type \<^ML_type>\<open>Symbol.sym\<close> is a concrete datatype that represents the
different kinds of symbols explicitly, with constructors
@@ -1387,7 +1385,7 @@
\<^enum> sequence of Isabelle symbols (see also \secref{sec:symbols}), with
\<^ML>\<open>Symbol.explode\<close> as key operation;
- \<^enum> XML tree structure via YXML (see also @{cite "isabelle-system"}), with
+ \<^enum> XML tree structure via YXML (see also \<^cite>\<open>"isabelle-system"\<close>), with
\<^ML>\<open>YXML.parse_body\<close> as key operation.
Note that Isabelle/ML string literals may refer Isabelle symbols like
@@ -1675,14 +1673,14 @@
exponential speedup of CPU performance due to ``Moore's Law'' follows
different rules: clock frequency has reached its peak around 2005, and
applications need to be parallelized in order to avoid a perceived loss of
- performance. See also @{cite "Sutter:2005"}.\<close>
+ performance. See also \<^cite>\<open>"Sutter:2005"\<close>.\<close>
Isabelle/Isar exploits the inherent structure of theories and proofs to
support \<^emph>\<open>implicit parallelism\<close> to a large extent. LCF-style theorem proving
- provides almost ideal conditions for that, see also @{cite "Wenzel:2009"}.
+ provides almost ideal conditions for that, see also \<^cite>\<open>"Wenzel:2009"\<close>.
This means, significant parts of theory and proof checking is parallelized
by default. In Isabelle2013, a maximum speedup-factor of 3.5 on 4 cores and
- 6.5 on 8 cores can be expected @{cite "Wenzel:2013:ITP"}.
+ 6.5 on 8 cores can be expected \<^cite>\<open>"Wenzel:2013:ITP"\<close>.
\<^medskip>
ML threads lack the memory protection of separate processes, and operate
@@ -2064,7 +2062,7 @@
text \<open>
Futures help to organize parallel execution in a value-oriented manner, with
\<open>fork\<close>~/ \<open>join\<close> as the main pair of operations, and some further variants;
- see also @{cite "Wenzel:2009" and "Wenzel:2013:ITP"}. Unlike lazy values,
+ see also \<^cite>\<open>"Wenzel:2009" and "Wenzel:2013:ITP"\<close>. Unlike lazy values,
futures are evaluated strictly and spontaneously on separate worker threads.
Futures may be canceled, which leads to interrupts on running evaluation
attempts, and forces structurally related futures to fail for all time;
--- a/src/Doc/Implementation/Prelim.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Implementation/Prelim.thy Sun Jan 15 18:30:18 2023 +0100
@@ -50,7 +50,7 @@
For example, there would be data for canonical introduction and elimination
rules for arbitrary operators (depending on the object-logic and
application), which enables users to perform standard proof steps implicitly
- (cf.\ the \<open>rule\<close> method @{cite "isabelle-isar-ref"}).
+ (cf.\ the \<open>rule\<close> method \<^cite>\<open>"isabelle-isar-ref"\<close>).
\<^medskip>
Thus Isabelle/Isar is able to bring forth more and more concepts
--- a/src/Doc/Implementation/Proof.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Implementation/Proof.thy Sun Jan 15 18:30:18 2023 +0100
@@ -361,7 +361,7 @@
means of a given tactic. This acts like a dual conclusion: the proof
demonstrates that the context may be augmented by parameters and
assumptions, without affecting any conclusions that do not mention these
- parameters. See also @{cite "isabelle-isar-ref"} for the corresponding Isar
+ parameters. See also \<^cite>\<open>"isabelle-isar-ref"\<close> for the corresponding Isar
proof command @{command obtain}. Final results, which may not refer to the
parameters in the conclusion, need to exported explicitly into the original
context.
--- a/src/Doc/Implementation/Syntax.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Implementation/Syntax.thy Sun Jan 15 18:30:18 2023 +0100
@@ -12,13 +12,13 @@
abstract syntax\<close> --- but end-users require additional means for reading and
printing of terms and types. This important add-on outside the logical core
is called \<^emph>\<open>inner syntax\<close> in Isabelle jargon, as opposed to the \<^emph>\<open>outer
- syntax\<close> of the theory and proof language @{cite "isabelle-isar-ref"}.
+ syntax\<close> of the theory and proof language \<^cite>\<open>"isabelle-isar-ref"\<close>.
- For example, according to @{cite church40} quantifiers are represented as
+ For example, according to \<^cite>\<open>church40\<close> quantifiers are represented as
higher-order constants \<open>All :: ('a \<Rightarrow> bool) \<Rightarrow> bool\<close> such that \<open>All (\<lambda>x::'a. B
x)\<close> faithfully represents the idea that is displayed in Isabelle as \<open>\<forall>x::'a.
B x\<close> via @{keyword "binder"} notation. Moreover, type-inference in the style
- of Hindley-Milner @{cite hindleymilner} (and extensions) enables users to
+ of Hindley-Milner \<^cite>\<open>hindleymilner\<close> (and extensions) enables users to
write \<open>\<forall>x. B x\<close> concisely, when the type \<open>'a\<close> is already clear from the
context.\<^footnote>\<open>Type-inference taken to the extreme can easily confuse users.
Beginners often stumble over unexpectedly general types inferred by the
@@ -121,8 +121,7 @@
\<^medskip>
Note that the string values that are passed in and out are annotated by the
- system, to carry further markup that is relevant for the Prover IDE @{cite
- "isabelle-jedit"}. User code should neither compose its own input strings,
+ system, to carry further markup that is relevant for the Prover IDE \<^cite>\<open>"isabelle-jedit"\<close>. User code should neither compose its own input strings,
nor try to analyze the output strings. Conceptually this is an abstract
datatype, encoded as concrete string for historical reasons.
@@ -150,8 +149,7 @@
declaratively via mixfix annotations. Moreover, there are \<^emph>\<open>syntax
translations\<close> that can be augmented by the user, either declaratively via
@{command translations} or programmatically via @{command
- parse_translation}, @{command print_translation} @{cite
- "isabelle-isar-ref"}. The final scope-resolution is performed by the system,
+ parse_translation}, @{command print_translation} \<^cite>\<open>"isabelle-isar-ref"\<close>. The final scope-resolution is performed by the system,
according to name spaces for types, term variables and constants determined
by the context.
\<close>
@@ -200,7 +198,7 @@
dual, it prunes type-information before pretty printing.
A typical add-on for the check/uncheck syntax layer is the @{command
- abbreviation} mechanism @{cite "isabelle-isar-ref"}. Here the user specifies
+ abbreviation} mechanism \<^cite>\<open>"isabelle-isar-ref"\<close>. Here the user specifies
syntactic definitions that are managed by the system as polymorphic \<open>let\<close>
bindings. These are expanded during the \<open>check\<close> phase, and contracted during
the \<open>uncheck\<close> phase, without affecting the type-assignment of the given
@@ -214,7 +212,7 @@
treats certain type instances of overloaded constants according to the
``dictionary construction'' of its logical foundation. This involves ``type
improvement'' (specialization of slightly too general types) and replacement
- by certain locale parameters. See also @{cite "Haftmann-Wenzel:2009"}.
+ by certain locale parameters. See also \<^cite>\<open>"Haftmann-Wenzel:2009"\<close>.
\<close>
text %mlref \<open>
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Sun Jan 15 18:30:18 2023 +0100
@@ -13,11 +13,11 @@
sources.
{\LaTeX} output is generated while processing a \<^emph>\<open>session\<close> in batch mode, as
- explained in the \<^emph>\<open>The Isabelle System Manual\<close> @{cite "isabelle-system"}.
+ explained in the \<^emph>\<open>The Isabelle System Manual\<close> \<^cite>\<open>"isabelle-system"\<close>.
The main Isabelle tools to get started with document preparation are
@{tool_ref mkroot} and @{tool_ref build}.
- The classic Isabelle/HOL tutorial @{cite "isabelle-hol-book"} also explains
+ The classic Isabelle/HOL tutorial \<^cite>\<open>"isabelle-hol-book"\<close> also explains
some aspects of theory presentation.
\<close>
@@ -324,8 +324,7 @@
characters, using some type-writer font style.
\<^descr> \<open>@{bash_function name}\<close> prints the given GNU bash function verbatim. The
- name is checked wrt.\ the Isabelle system environment @{cite
- "isabelle-system"}.
+ name is checked wrt.\ the Isabelle system environment \<^cite>\<open>"isabelle-system"\<close>.
\<^descr> \<open>@{system_option name}\<close> prints the given system option verbatim. The name
is checked wrt.\ cumulative \<^verbatim>\<open>etc/options\<close> of all Isabelle components,
@@ -605,7 +604,7 @@
\end{tabular}
\<^medskip>
- The Isabelle document preparation system @{cite "isabelle-system"} allows
+ The Isabelle document preparation system \<^cite>\<open>"isabelle-system"\<close> allows
tagged command regions to be presented specifically, e.g.\ to fold proof
texts, or drop parts of the text completely.
@@ -627,7 +626,7 @@
the meaning of arbitrary tags to ``keep'', ``drop'', or ``fold'' the
corresponding parts of the text. Logic sessions may also specify ``document
versions'', where given tags are interpreted in some particular way. Again
- see @{cite "isabelle-system"} for further details.
+ see \<^cite>\<open>"isabelle-system"\<close> for further details.
\<close>
--- a/src/Doc/Isar_Ref/First_Order_Logic.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Isar_Ref/First_Order_Logic.thy Sun Jan 15 18:30:18 2023 +0100
@@ -164,7 +164,7 @@
text \<open>
We axiomatize basic connectives of propositional logic: implication,
disjunction, and conjunction. The associated rules are modeled after
- Gentzen's system of Natural Deduction @{cite "Gentzen:1935"}.
+ Gentzen's system of Natural Deduction \<^cite>\<open>"Gentzen:1935"\<close>.
\<close>
axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longrightarrow>" 25)
@@ -315,7 +315,7 @@
text \<open>
Representing quantifiers is easy, thanks to the higher-order nature of the
underlying framework. According to the well-known technique introduced by
- Church @{cite "church40"}, quantifiers are operators on predicates, which
+ Church \<^cite>\<open>"church40"\<close>, quantifiers are operators on predicates, which
are syntactically represented as \<open>\<lambda>\<close>-terms of type \<^typ>\<open>i \<Rightarrow> o\<close>. Binder
notation turns \<open>All (\<lambda>x. B x)\<close> into \<open>\<forall>x. B x\<close> etc.
\<close>
--- a/src/Doc/Isar_Ref/Framework.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Isar_Ref/Framework.thy Sun Jan 15 18:30:18 2023 +0100
@@ -7,9 +7,9 @@
chapter \<open>The Isabelle/Isar Framework \label{ch:isar-framework}\<close>
text \<open>
- Isabelle/Isar @{cite "Wenzel:1999:TPHOL" and "Wenzel-PhD" and
+ Isabelle/Isar \<^cite>\<open>"Wenzel:1999:TPHOL" and "Wenzel-PhD" and
"Nipkow-TYPES02" and "Wiedijk:1999:Mizar" and "Wenzel-Paulson:2006" and
- "Wenzel:2006:Festschrift"} is a generic framework for developing formal
+ "Wenzel:2006:Festschrift"\<close> is a generic framework for developing formal
mathematical documents with full proof checking. Definitions, statements and
proofs are organized as theories. A collection of theories sources may be
presented as a printed document; see also \chref{ch:document-prep}.
@@ -32,10 +32,9 @@
intelligible text to the human reader.
The Isar proof language has emerged from careful analysis of some inherent
- virtues of the logical framework Isabelle/Pure @{cite "paulson-found" and
- "paulson700"}, notably composition of higher-order natural deduction rules,
- which is a generalization of Gentzen's original calculus @{cite
- "Gentzen:1935"}. The approach of generic inference systems in Pure is
+ virtues of the logical framework Isabelle/Pure \<^cite>\<open>"paulson-found" and
+ "paulson700"\<close>, notably composition of higher-order natural deduction rules,
+ which is a generalization of Gentzen's original calculus \<^cite>\<open>"Gentzen:1935"\<close>. The approach of generic inference systems in Pure is
continued by Isar towards actual proof texts. See also
\figref{fig:natural-deduction}
@@ -88,14 +87,13 @@
\<^medskip>
Concrete applications require another intermediate layer: an object-logic.
- Isabelle/HOL @{cite "isa-tutorial"} (simply-typed set-theory) is most
+ Isabelle/HOL \<^cite>\<open>"isa-tutorial"\<close> (simply-typed set-theory) is most
commonly used; elementary examples are given in the directories
\<^dir>\<open>~~/src/Pure/Examples\<close> and \<^dir>\<open>~~/src/HOL/Examples\<close>. Some examples
demonstrate how to start a fresh object-logic from Isabelle/Pure, and use
Isar proofs from the very start, despite the lack of advanced proof tools at
such an early stage (e.g.\ see
- \<^file>\<open>~~/src/Pure/Examples/Higher_Order_Logic.thy\<close>). Isabelle/FOL @{cite
- "isabelle-logics"} and Isabelle/ZF @{cite "isabelle-ZF"} also work, but are
+ \<^file>\<open>~~/src/Pure/Examples/Higher_Order_Logic.thy\<close>). Isabelle/FOL \<^cite>\<open>"isabelle-logics"\<close> and Isabelle/ZF \<^cite>\<open>"isabelle-ZF"\<close> also work, but are
much less developed.
In order to illustrate natural deduction in Isar, we shall subsequently
@@ -276,8 +274,8 @@
section \<open>The Pure framework \label{sec:framework-pure}\<close>
text \<open>
- The Pure logic @{cite "paulson-found" and "paulson700"} is an intuitionistic
- fragment of higher-order logic @{cite "church40"}. In type-theoretic
+ The Pure logic \<^cite>\<open>"paulson-found" and "paulson700"\<close> is an intuitionistic
+ fragment of higher-order logic \<^cite>\<open>"church40"\<close>. In type-theoretic
parlance, there are three levels of \<open>\<lambda>\<close>-calculus with corresponding arrows
\<open>\<Rightarrow>\<close>/\<open>\<And>\<close>/\<open>\<Longrightarrow>\<close>:
@@ -291,14 +289,13 @@
Here only the types of syntactic terms, and the propositions of proof terms
have been shown. The \<open>\<lambda>\<close>-structure of proofs can be recorded as an optional
- feature of the Pure inference kernel @{cite "Berghofer-Nipkow:2000:TPHOL"},
+ feature of the Pure inference kernel \<^cite>\<open>"Berghofer-Nipkow:2000:TPHOL"\<close>,
but the formal system can never depend on them due to \<^emph>\<open>proof irrelevance\<close>.
On top of this most primitive layer of proofs, Pure implements a generic
- calculus for nested natural deduction rules, similar to @{cite
- "Schroeder-Heister:1984"}. Here object-logic inferences are internalized as
+ calculus for nested natural deduction rules, similar to \<^cite>\<open>"Schroeder-Heister:1984"\<close>. Here object-logic inferences are internalized as
formulae over \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close>. Combining such rule statements may involve
- higher-order unification @{cite "paulson-natural"}.
+ higher-order unification \<^cite>\<open>"paulson-natural"\<close>.
\<close>
@@ -364,8 +361,7 @@
connectives \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> commute. So we may assume w.l.o.g.\ that rule
statements always observe the normal form where quantifiers are pulled in
front of implications at each level of nesting. This means that any Pure
- proposition may be presented as a \<^emph>\<open>Hereditary Harrop Formula\<close> @{cite
- "Miller:1991"} which is of the form \<open>\<And>x\<^sub>1 \<dots> x\<^sub>m. H\<^sub>1 \<Longrightarrow> \<dots> H\<^sub>n \<Longrightarrow> A\<close> for \<open>m, n
+ proposition may be presented as a \<^emph>\<open>Hereditary Harrop Formula\<close> \<^cite>\<open>"Miller:1991"\<close> which is of the form \<open>\<And>x\<^sub>1 \<dots> x\<^sub>m. H\<^sub>1 \<Longrightarrow> \<dots> H\<^sub>n \<Longrightarrow> A\<close> for \<open>m, n
\<ge> 0\<close>, and \<open>A\<close> atomic, and \<open>H\<^sub>1, \<dots>, H\<^sub>n\<close> being recursively of the same
format. Following the convention that outermost quantifiers are implicit,
Horn clauses \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A\<close> are a special case of this.
@@ -572,7 +568,7 @@
may be populated later. The command \<^theory_text>\<open>method_setup\<close> allows to define proof
methods semantically in Isabelle/ML. The Eisbach language allows to define
proof methods symbolically, as recursive expressions over existing methods
- @{cite "Matichuk-et-al:2014"}; see also \<^dir>\<open>~~/src/HOL/Eisbach\<close>.
+ \<^cite>\<open>"Matichuk-et-al:2014"\<close>; see also \<^dir>\<open>~~/src/HOL/Eisbach\<close>.
Methods use the facts indicated by \<^theory_text>\<open>then\<close> or \<^theory_text>\<open>using\<close>, and then operate on
the goal state. Some basic methods are predefined in Pure: ``@{method "-"}''
@@ -635,8 +631,7 @@
\]
\<^medskip>
- The most interesting derived context element in Isar is \<^theory_text>\<open>obtain\<close> @{cite
- \<open>\S5.3\<close> "Wenzel-PhD"}, which supports generalized elimination steps in a
+ The most interesting derived context element in Isar is \<^theory_text>\<open>obtain\<close> \<^cite>\<open>\<open>\S5.3\<close> in "Wenzel-PhD"\<close>, which supports generalized elimination steps in a
purely forward manner. The \<^theory_text>\<open>obtain\<close> command takes a specification of
parameters \<open>\<^vec>x\<close> and assumptions \<open>\<^vec>A\<close> to be added to the context,
together with a proof of a case rule stating that this extension is
@@ -971,8 +966,7 @@
etc. Due to the flexibility of rule composition
(\secref{sec:framework-resolution}), substitution of equals by equals is
covered as well, even substitution of inequalities involving monotonicity
- conditions; see also @{cite \<open>\S6\<close> "Wenzel-PhD"} and @{cite
- "Bauer-Wenzel:2001"}.
+ conditions; see also \<^cite>\<open>\<open>\S6\<close> in "Wenzel-PhD"\<close> and \<^cite>\<open>"Bauer-Wenzel:2001"\<close>.
The generic calculational mechanism is based on the observation that rules
such as \<open>trans:\<close>~\<^prop>\<open>x = y \<Longrightarrow> y = z \<Longrightarrow> x = z\<close> proceed from the premises
--- a/src/Doc/Isar_Ref/Generic.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy Sun Jan 15 18:30:18 2023 +0100
@@ -95,8 +95,7 @@
\<^descr> @{method erule}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close>, @{method drule}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close>, and @{method
frule}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> are similar to the basic @{method rule} method (see
\secref{sec:pure-meth-att}), but apply rules by elim-resolution,
- destruct-resolution, and forward-resolution, respectively @{cite
- "isabelle-implementation"}. The optional natural number argument (default 0)
+ destruct-resolution, and forward-resolution, respectively \<^cite>\<open>"isabelle-implementation"\<close>. The optional natural number argument (default 0)
specifies additional assumption steps to be performed here.
Note that these methods are improper ones, mainly serving for
@@ -153,7 +152,7 @@
\<^descr> @{attribute THEN}~\<open>a\<close> composes rules by resolution; it resolves with the
first premise of \<open>a\<close> (an alternative position may be also specified). See
- also \<^ML_infix>\<open>RS\<close> in @{cite "isabelle-implementation"}.
+ also \<^ML_infix>\<open>RS\<close> in \<^cite>\<open>"isabelle-implementation"\<close>.
\<^descr> @{attribute unfolded}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> and @{attribute folded}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close>
expand and fold back again the given definitions throughout a rule.
@@ -520,7 +519,7 @@
\<open>(?x + ?y) + ?z \<equiv> ?x + (?y + ?z)\<close> \\
\<open>f (f ?x ?y) ?z \<equiv> f ?x (f ?y ?z)\<close>
- \<^enum> Higher-order patterns in the sense of @{cite "nipkow-patterns"}. These
+ \<^enum> Higher-order patterns in the sense of \<^cite>\<open>"nipkow-patterns"\<close>. These
are terms in \<open>\<beta>\<close>-normal form (this will always be the case unless you have
done something strange) where each occurrence of an unknown is of the form
\<open>?F x\<^sub>1 \<dots> x\<^sub>n\<close>, where the \<open>x\<^sub>i\<close> are distinct bound variables.
@@ -701,9 +700,9 @@
end
text \<open>
- Martin and Nipkow @{cite "martin-nipkow"} discuss the theory and give many
+ Martin and Nipkow \<^cite>\<open>"martin-nipkow"\<close> discuss the theory and give many
examples; other algebraic structures are amenable to ordered rewriting, such
- as Boolean rings. The Boyer-Moore theorem prover @{cite bm88book} also
+ as Boolean rings. The Boyer-Moore theorem prover \<^cite>\<open>bm88book\<close> also
employs ordered rewriting.
\<close>
@@ -756,7 +755,7 @@
simplification procedures.
\<^descr> @{attribute simp_trace_new} controls Simplifier tracing within
- Isabelle/PIDE applications, notably Isabelle/jEdit @{cite "isabelle-jedit"}.
+ Isabelle/PIDE applications, notably Isabelle/jEdit \<^cite>\<open>"isabelle-jedit"\<close>.
This provides a hierarchical representation of the rewriting steps performed
by the Simplifier.
@@ -1115,7 +1114,7 @@
context. These proof procedures are slow and simplistic compared
with high-end automated theorem provers, but they can save
considerable time and effort in practice. They can prove theorems
- such as Pelletier's @{cite pelletier86} problems 40 and 41 in a few
+ such as Pelletier's \<^cite>\<open>pelletier86\<close> problems 40 and 41 in a few
milliseconds (including full proof reconstruction):\<close>
lemma "(\<exists>y. \<forall>x. F x y \<longleftrightarrow> F x x) \<longrightarrow> \<not> (\<forall>x. \<exists>y. \<forall>z. F z y \<longleftrightarrow> \<not> F z x)"
@@ -1186,8 +1185,8 @@
desired theorem and apply rules backwards in a fairly arbitrary
manner. This yields a surprisingly effective proof procedure.
Quantifiers add only few complications, since Isabelle handles
- parameters and schematic variables. See @{cite \<open>Chapter 10\<close>
- "paulson-ml2"} for further discussion.\<close>
+ parameters and schematic variables. See \<^cite>\<open>\<open>Chapter 10\<close> in
+ "paulson-ml2"\<close> for further discussion.\<close>
subsubsection \<open>Simulating sequents by natural deduction\<close>
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Sun Jan 15 18:30:18 2023 +0100
@@ -18,16 +18,16 @@
Isabelle/HOL is based on Higher-Order Logic, a polymorphic version of
Church's Simple Theory of Types. HOL can be best understood as a
simply-typed version of classical set theory. The logic was first
- implemented in Gordon's HOL system @{cite "mgordon-hol"}. It extends
- Church's original logic @{cite "church40"} by explicit type variables (naive
+ implemented in Gordon's HOL system \<^cite>\<open>"mgordon-hol"\<close>. It extends
+ Church's original logic \<^cite>\<open>"church40"\<close> by explicit type variables (naive
polymorphism) and a sound axiomatization scheme for new types based on
subsets of existing types.
- Andrews's book @{cite andrews86} is a full description of the original
+ Andrews's book \<^cite>\<open>andrews86\<close> is a full description of the original
Church-style higher-order logic, with proofs of correctness and completeness
wrt.\ certain set-theoretic interpretations. The particular extensions of
Gordon-style HOL are explained semantically in two chapters of the 1993 HOL
- book @{cite pitts93}.
+ book \<^cite>\<open>pitts93\<close>.
Experience with HOL over decades has demonstrated that higher-order logic is
widely applicable in many areas of mathematics and computer science. In a
@@ -238,7 +238,7 @@
text \<open>
Here the \<open>cases\<close> or \<open>induct\<close> rules produced by the @{command inductive}
package coincide with the expected elimination rules for Natural Deduction.
- Already in the original article by Gerhard Gentzen @{cite "Gentzen:1935"}
+ Already in the original article by Gerhard Gentzen \<^cite>\<open>"Gentzen:1935"\<close>
there is a hint that each connective can be characterized by its
introductions, and the elimination can be constructed systematically.
\<close>
@@ -289,8 +289,7 @@
simulating symbolic computation via rewriting.
\<^descr> @{command (HOL) "function"} defines functions by general wellfounded
- recursion. A detailed description with examples can be found in @{cite
- "isabelle-function"}. The function is specified by a set of (possibly
+ recursion. A detailed description with examples can be found in \<^cite>\<open>"isabelle-function"\<close>. The function is specified by a set of (possibly
conditional) recursive equations with arbitrary pattern matching. The
command generates proof obligations for the completeness and the
compatibility of patterns.
@@ -302,7 +301,7 @@
\<^descr> @{command (HOL) "fun"} is a shorthand notation for ``@{command (HOL)
"function"}~\<open>(sequential)\<close>'', followed by automated proof attempts regarding
- pattern matching and termination. See @{cite "isabelle-function"} for
+ pattern matching and termination. See \<^cite>\<open>"isabelle-function"\<close> for
further details.
\<^descr> @{command (HOL) "termination"}~\<open>f\<close> commences a termination proof for the
@@ -507,7 +506,7 @@
\<^descr> @{method (HOL) pat_completeness} is a specialized method to solve goals
regarding the completeness of pattern matching, as required by the @{command
- (HOL) "function"} package (cf.\ @{cite "isabelle-function"}).
+ (HOL) "function"} package (cf.\ \<^cite>\<open>"isabelle-function"\<close>).
\<^descr> @{method (HOL) relation}~\<open>R\<close> introduces a termination proof using the
relation \<open>R\<close>. The resulting proof state will contain goals expressing that
@@ -523,11 +522,11 @@
@{method auto}).
In case of failure, extensive information is printed, which can help to
- analyse the situation (cf.\ @{cite "isabelle-function"}).
+ analyse the situation (cf.\ \<^cite>\<open>"isabelle-function"\<close>).
\<^descr> @{method (HOL) "size_change"} also works on termination goals, using a
variation of the size-change principle, together with a graph decomposition
- technique (see @{cite krauss_phd} for details). Three kinds of orders are
+ technique (see \<^cite>\<open>krauss_phd\<close> for details). Three kinds of orders are
used internally: \<open>max\<close>, \<open>min\<close>, and \<open>ms\<close> (multiset), which is only available
when the theory \<open>Multiset\<close> is loaded. When no order kinds are given, they
are tried in order. The search for a termination proof uses SAT solving
@@ -734,7 +733,7 @@
These commands are mostly obsolete; @{command (HOL) "datatype"} should be
used instead.
- See @{cite "isabelle-datatypes"} for more details on datatypes. Apart from
+ See \<^cite>\<open>"isabelle-datatypes"\<close> for more details on datatypes. Apart from
proper proof methods for case analysis and induction, there are also
emulations of ML tactics @{method (HOL) case_tac} and @{method (HOL)
induct_tac} available, see \secref{sec:hol-induct-tac}; these admit to refer
@@ -785,7 +784,7 @@
infrastructure of records in Isabelle/HOL is slightly more advanced, though,
supporting truly extensible record schemes. This admits operations that are
polymorphic with respect to record extension, yielding ``object-oriented''
- effects like (single) inheritance. See also @{cite "NaraschewskiW-TPHOLs98"}
+ effects like (single) inheritance. See also \<^cite>\<open>"NaraschewskiW-TPHOLs98"\<close>
for more details on object-oriented verification and record subtyping in
HOL.
\<close>
@@ -841,7 +840,7 @@
of fields as given by their declaration. The record package provides several
standard operations like selectors and updates. The common setup for various
generic proof tools enable succinct reasoning patterns. See also the
- Isabelle/HOL tutorial @{cite "isabelle-hol-book"} for further instructions
+ Isabelle/HOL tutorial \<^cite>\<open>"isabelle-hol-book"\<close> for further instructions
on using records in practice.
\<close>
@@ -1041,25 +1040,25 @@
To understand the concept of type definition better, we need to recount its
somewhat complex history. The HOL logic goes back to the ``Simple Theory of
- Types'' (STT) of A. Church @{cite "church40"}, which is further explained in
- the book by P. Andrews @{cite "andrews86"}. The overview article by W.
- Farmer @{cite "Farmer:2008"} points out the ``seven virtues'' of this
+ Types'' (STT) of A. Church \<^cite>\<open>"church40"\<close>, which is further explained in
+ the book by P. Andrews \<^cite>\<open>"andrews86"\<close>. The overview article by W.
+ Farmer \<^cite>\<open>"Farmer:2008"\<close> points out the ``seven virtues'' of this
relatively simple family of logics. STT has only ground types, without
polymorphism and without type definitions.
\<^medskip>
- M. Gordon @{cite "Gordon:1985:HOL"} augmented Church's STT by adding
+ M. Gordon \<^cite>\<open>"Gordon:1985:HOL"\<close> augmented Church's STT by adding
schematic polymorphism (type variables and type constructors) and a facility
to introduce new types as semantic subtypes from existing types. This
genuine extension of the logic was explained semantically by A. Pitts in the
- book of the original Cambridge HOL88 system @{cite "pitts93"}. Type
+ book of the original Cambridge HOL88 system \<^cite>\<open>"pitts93"\<close>. Type
definitions work in this setting, because the general model-theory of STT is
restricted to models that ensure that the universe of type interpretations
is closed by forming subsets (via predicates taken from the logic).
\<^medskip>
Isabelle/HOL goes beyond Gordon-style HOL by admitting overloaded constant
- definitions @{cite "Wenzel:1997:TPHOL" and "Haftmann-Wenzel:2006:classes"},
+ definitions \<^cite>\<open>"Wenzel:1997:TPHOL" and "Haftmann-Wenzel:2006:classes"\<close>,
which are actually a concept of Isabelle/Pure and do not depend on
particular set-theoretic semantics of HOL. Over many years, there was no
formal checking of semantic type definitions in Isabelle/HOL versus
@@ -1068,11 +1067,10 @@
\secref{sec:axiomatizations}, only with some local checks of the given type
and its representing set.
- Recent clarification of overloading in the HOL logic proper @{cite
- "Kuncar-Popescu:2015"} demonstrates how the dissimilar concepts of constant
+ Recent clarification of overloading in the HOL logic proper \<^cite>\<open>"Kuncar-Popescu:2015"\<close> demonstrates how the dissimilar concepts of constant
definitions versus type definitions may be understood uniformly. This
requires an interpretation of Isabelle/HOL that substantially reforms the
- set-theoretic model of A. Pitts @{cite "pitts93"}, by taking a schematic
+ set-theoretic model of A. Pitts \<^cite>\<open>"pitts93"\<close>, by taking a schematic
view on polymorphism and interpreting only ground types in the set-theoretic
sense of HOL88. Moreover, type-constructors may be explicitly overloaded,
e.g.\ by making the subset depend on type-class parameters (cf.\
@@ -1256,8 +1254,7 @@
package works with all four kinds of type abstraction: type copies,
subtypes, total quotients and partial quotients.
- Theoretical background can be found in @{cite
- "Huffman-Kuncar:2013:lifting_transfer"}.
+ Theoretical background can be found in \<^cite>\<open>"Huffman-Kuncar:2013:lifting_transfer"\<close>.
\begin{matharray}{rcl}
@{command_def (HOL) "setup_lifting"} & : & \<open>local_theory \<rightarrow> local_theory\<close>\\
@@ -1459,7 +1456,7 @@
(HOL) lifting_forget} and @{command (HOL) lifting_update} is preferred for
normal usage.
- \<^descr> Integration with the BNF package @{cite "isabelle-datatypes"}: As already
+ \<^descr> Integration with the BNF package \<^cite>\<open>"isabelle-datatypes"\<close>: As already
mentioned, the theorems that are registered by the following attributes are
proved and registered automatically if the involved type is BNF without dead
variables: @{attribute (HOL) quot_map}, @{attribute (HOL) relator_eq_onp},
@@ -1545,8 +1542,7 @@
Preservation of predicates on relations (\<open>bi_unique, bi_total, right_unique,
right_total, left_unique, left_total\<close>) with the respect to a relator is
- proved automatically if the involved type is BNF @{cite
- "isabelle-datatypes"} without dead variables.
+ proved automatically if the involved type is BNF \<^cite>\<open>"isabelle-datatypes"\<close> without dead variables.
\<^descr> @{attribute (HOL) "transfer_domain_rule"} attribute maintains a collection
of rules, which specify a domain of a transfer relation by a predicate.
@@ -1570,8 +1566,7 @@
is proved automatically if the involved type is BNF without dead variables.
- Theoretical background can be found in @{cite
- "Huffman-Kuncar:2013:lifting_transfer"}.
+ Theoretical background can be found in \<^cite>\<open>"Huffman-Kuncar:2013:lifting_transfer"\<close>.
\<close>
@@ -1723,7 +1718,7 @@
\<^descr> @{command (HOL) "sledgehammer"} attempts to prove a subgoal using external
automatic provers (resolution provers and SMT solvers). See the Sledgehammer
- manual @{cite "isabelle-sledgehammer"} for details.
+ manual \<^cite>\<open>"isabelle-sledgehammer"\<close> for details.
\<^descr> @{command (HOL) "sledgehammer_params"} changes @{command (HOL)
"sledgehammer"} configuration options persistently.
@@ -1876,8 +1871,7 @@
and a lazy term reconstruction of the value in the type \<^typ>\<open>Code_Evaluation.term\<close>. A pseudo-randomness generator is defined in theory
\<^theory>\<open>HOL.Random\<close>.
- \<^descr>[\<open>narrowing\<close>] implements Haskell's Lazy Smallcheck @{cite
- "runciman-naylor-lindblad"} using the type classes \<^class>\<open>narrowing\<close> and
+ \<^descr>[\<open>narrowing\<close>] implements Haskell's Lazy Smallcheck \<^cite>\<open>"runciman-naylor-lindblad"\<close> using the type classes \<^class>\<open>narrowing\<close> and
\<^class>\<open>partial_term_of\<close>. Variables in the current goal are initially
represented as symbolic variables. If the execution of the goal tries to
evaluate one of them, the test engine replaces it with refinements
@@ -1918,7 +1912,7 @@
\<^descr> @{command (HOL) "nitpick"} tests the current goal for counterexamples
using a reduction to first-order relational logic. See the Nitpick manual
- @{cite "isabelle-nitpick"} for details.
+ \<^cite>\<open>"isabelle-nitpick"\<close> for details.
\<^descr> @{command (HOL) "nitpick_params"} changes @{command (HOL) "nitpick"}
configuration options persistently.
@@ -1944,7 +1938,7 @@
Coercive subtyping allows the user to omit explicit type conversions, also
called \<^emph>\<open>coercions\<close>. Type inference will add them as necessary when parsing
- a term. See @{cite "traytel-berghofer-nipkow-2011"} for details.
+ a term. See \<^cite>\<open>"traytel-berghofer-nipkow-2011"\<close> for details.
\<^rail>\<open>
@@{attribute (HOL) coercion} (@{syntax term})
@@ -2065,12 +2059,12 @@
\<close>
\<^descr> @{method (HOL) meson} implements Loveland's model elimination procedure
- @{cite "loveland-78"}. See \<^file>\<open>~~/src/HOL/ex/Meson_Test.thy\<close> for examples.
+ \<^cite>\<open>"loveland-78"\<close>. See \<^file>\<open>~~/src/HOL/ex/Meson_Test.thy\<close> for examples.
\<^descr> @{method (HOL) metis} combines ordered resolution and ordered
paramodulation to find first-order (or mildly higher-order) proofs. The
first optional argument specifies a type encoding; see the Sledgehammer
- manual @{cite "isabelle-sledgehammer"} for details. The directory
+ manual \<^cite>\<open>"isabelle-sledgehammer"\<close> for details. The directory
\<^dir>\<open>~~/src/HOL/Metis_Examples\<close> contains several small theories developed to a
large extent using @{method (HOL) metis}.
\<close>
@@ -2093,7 +2087,7 @@
\<close>
\<^descr> @{method (HOL) algebra} performs algebraic reasoning via Gröbner bases,
- see also @{cite "Chaieb-Wenzel:2007"} and @{cite \<open>\S3.2\<close> "Chaieb-thesis"}.
+ see also \<^cite>\<open>"Chaieb-Wenzel:2007"\<close> and \<^cite>\<open>\<open>\S3.2\<close> in "Chaieb-thesis"\<close>.
The method handles deals with two main classes of problems:
\<^enum> Universal problems over multivariate polynomials in a
@@ -2165,8 +2159,7 @@
@@{method (HOL) coherent} @{syntax thms}?
\<close>
- \<^descr> @{method (HOL) coherent} solves problems of \<^emph>\<open>Coherent Logic\<close> @{cite
- "Bezem-Coquand:2005"}, which covers applications in confluence theory,
+ \<^descr> @{method (HOL) coherent} solves problems of \<^emph>\<open>Coherent Logic\<close> \<^cite>\<open>"Bezem-Coquand:2005"\<close>, which covers applications in confluence theory,
lattice theory and projective geometry. See \<^file>\<open>~~/src/HOL/Examples/Coherent.thy\<close>
for some examples.
\<close>
@@ -2258,13 +2251,12 @@
executable specifications. Isabelle/HOL instantiates these mechanisms in a
way that is amenable to end-user applications. Code can be generated for
functional programs (including overloading using type classes) targeting SML
- @{cite SML}, OCaml @{cite OCaml}, Haskell @{cite "haskell-revised-report"}
- and Scala @{cite "scala-overview-tech-report"}. Conceptually, code
+ \<^cite>\<open>SML\<close>, OCaml \<^cite>\<open>OCaml\<close>, Haskell \<^cite>\<open>"haskell-revised-report"\<close>
+ and Scala \<^cite>\<open>"scala-overview-tech-report"\<close>. Conceptually, code
generation is split up in three steps: \<^emph>\<open>selection\<close> of code theorems,
\<^emph>\<open>translation\<close> into an abstract executable view and \<^emph>\<open>serialization\<close> to a
specific \<^emph>\<open>target language\<close>. Inductive specifications can be executed using
- the predicate compiler which operates within HOL. See @{cite
- "isabelle-codegen"} for an introduction.
+ the predicate compiler which operates within HOL. See \<^cite>\<open>"isabelle-codegen"\<close> for an introduction.
\begin{matharray}{rcl}
@{command_def (HOL) "export_code"}\<open>\<^sup>*\<close> & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Sun Jan 15 18:30:18 2023 +0100
@@ -100,7 +100,7 @@
particular print mode features. For example, @{command
"print_state"}~\<open>(latex)\<close> prints the current proof state with mathematical
symbols and special characters represented in {\LaTeX} source, according to
- the Isabelle style @{cite "isabelle-system"}.
+ the Isabelle style \<^cite>\<open>"isabelle-system"\<close>.
Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more systematic
way to include formal items into the printed text document.
@@ -273,7 +273,7 @@
to abstract syntax, and the pretty printing. Special case annotations
provide a simple means of specifying infix operators and binders.
- Isabelle mixfix syntax is inspired by {\OBJ} @{cite OBJ}. It allows to
+ Isabelle mixfix syntax is inspired by {\OBJ} \<^cite>\<open>OBJ\<close>. It allows to
specify any context-free priority grammar, which is more general than the
fixity declarations of ML and Prolog.
@@ -411,7 +411,7 @@
\<^medskip>
Note that the general idea of pretty printing with blocks and breaks is
- described in @{cite "paulson-ml2"}; it goes back to @{cite "Oppen:1980"}.
+ described in \<^cite>\<open>"paulson-ml2"\<close>; it goes back to \<^cite>\<open>"Oppen:1980"\<close>.
\<close>
@@ -452,7 +452,7 @@
text \<open>
A \<^emph>\<open>binder\<close> is a variable-binding construct such as a quantifier. The idea
to formalize \<open>\<forall>x. b\<close> as \<open>All (\<lambda>x. b)\<close> for \<open>All :: ('a \<Rightarrow> bool) \<Rightarrow> bool\<close>
- already goes back to @{cite church40}. Isabelle declarations of certain
+ already goes back to \<^cite>\<open>church40\<close>. Isabelle declarations of certain
higher-order operators may be annotated with @{keyword_def "binder"}
annotations as follows:
@@ -955,8 +955,7 @@
carefully by syntax transformations.
Pre-terms are further processed by the so-called \<^emph>\<open>check\<close> and \<^emph>\<open>uncheck\<close>
- phases that are intertwined with type-inference (see also @{cite
- "isabelle-implementation"}). The latter allows to operate on higher-order
+ phases that are intertwined with type-inference (see also \<^cite>\<open>"isabelle-implementation"\<close>). The latter allows to operate on higher-order
abstract syntax with proper binding and type information already available.
As a rule of thumb, anything that manipulates bindings of variables or
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Sun Jan 15 18:30:18 2023 +0100
@@ -26,8 +26,7 @@
theory, while \<^verbatim>\<open>x + y\<close> without quotes is not.
Printed theory documents usually omit quotes to gain readability (this is a
- matter of {\LaTeX} macro setup, say via \<^verbatim>\<open>\isabellestyle\<close>, see also @{cite
- "isabelle-system"}). Experienced users of Isabelle/Isar may easily
+ matter of {\LaTeX} macro setup, say via \<^verbatim>\<open>\isabellestyle\<close>, see also \<^cite>\<open>"isabelle-system"\<close>). Experienced users of Isabelle/Isar may easily
reconstruct the lost technical information, while mere readers need not care
about quotes at all.
\<close>
--- a/src/Doc/Isar_Ref/Preface.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Isar_Ref/Preface.thy Sun Jan 15 18:30:18 2023 +0100
@@ -20,19 +20,19 @@
transactions with unlimited undo etc.
In its pioneering times, the Isabelle/Isar version of the
- \<^emph>\<open>Proof~General\<close> user interface @{cite proofgeneral and
- "Aspinall:TACAS:2000"} has contributed to the
+ \<^emph>\<open>Proof~General\<close> user interface \<^cite>\<open>proofgeneral and
+ "Aspinall:TACAS:2000"\<close> has contributed to the
success of for interactive theory and proof development in this
advanced theorem proving environment, even though it was somewhat
biased towards old-style proof scripts. The more recent
- Isabelle/jEdit Prover IDE @{cite "Wenzel:2012"} emphasizes the
+ Isabelle/jEdit Prover IDE \<^cite>\<open>"Wenzel:2012"\<close> emphasizes the
document-oriented approach of Isabelle/Isar again more explicitly.
\<^medskip>
Apart from the technical advances over bare-bones ML
programming, the main purpose of the Isar language is to provide a
conceptually different view on machine-checked proofs
- @{cite "Wenzel:1999:TPHOL" and "Wenzel-PhD"}. \<^emph>\<open>Isar\<close> stands for
+ \<^cite>\<open>"Wenzel:1999:TPHOL" and "Wenzel-PhD"\<close>. \<^emph>\<open>Isar\<close> stands for
\<^emph>\<open>Intelligible semi-automated reasoning\<close>. Drawing from both the
traditions of informal mathematical proof texts and high-level
programming languages, Isar offers a versatile environment for
--- a/src/Doc/Isar_Ref/Proof.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Isar_Ref/Proof.thy Sun Jan 15 18:30:18 2023 +0100
@@ -626,7 +626,7 @@
applied with restriction to the first subgoal, then \<open>m\<^sub>2\<close> is applied
consecutively with restriction to each subgoal that has newly emerged due to
\<open>m\<^sub>1\<close>. This is analogous to the tactic combinator \<^ML_infix>\<open>THEN_ALL_NEW\<close> in
- Isabelle/ML, see also @{cite "isabelle-implementation"}. For example, \<open>(rule
+ Isabelle/ML, see also \<^cite>\<open>"isabelle-implementation"\<close>. For example, \<open>(rule
r; blast)\<close> applies rule \<open>r\<close> and then solves all new subgoals by \<open>blast\<close>.
Moreover, the explicit goal restriction operator ``\<open>[n]\<close>'' exposes only the
--- a/src/Doc/Isar_Ref/Proof_Script.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Isar_Ref/Proof_Script.thy Sun Jan 15 18:30:18 2023 +0100
@@ -236,11 +236,10 @@
\<close>
\<^descr> @{method rule_tac} etc. do resolution of rules with explicit
- instantiation. This works the same way as the ML tactics \<^ML>\<open>Rule_Insts.res_inst_tac\<close> etc.\ (see @{cite "isabelle-implementation"}).
+ instantiation. This works the same way as the ML tactics \<^ML>\<open>Rule_Insts.res_inst_tac\<close> etc.\ (see \<^cite>\<open>"isabelle-implementation"\<close>).
Multiple rules may be only given if there is no instantiation; then @{method
- rule_tac} is the same as \<^ML>\<open>resolve_tac\<close> in ML (see @{cite
- "isabelle-implementation"}).
+ rule_tac} is the same as \<^ML>\<open>resolve_tac\<close> in ML (see \<^cite>\<open>"isabelle-implementation"\<close>).
\<^descr> @{method cut_tac} inserts facts into the proof state as assumption of a
subgoal; instantiations may be given as well. Note that the scope of
--- a/src/Doc/Isar_Ref/Spec.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy Sun Jan 15 18:30:18 2023 +0100
@@ -456,7 +456,7 @@
this process, which is called \<^emph>\<open>roundup\<close>, redundant locale instances are
omitted. A locale instance is redundant if it is subsumed by an instance
encountered earlier. A more detailed description of this process is
- available elsewhere @{cite Ballarin2014}.
+ available elsewhere \<^cite>\<open>Ballarin2014\<close>.
\<close>
@@ -835,10 +835,10 @@
A class is a particular locale with \<^emph>\<open>exactly one\<close> type variable \<open>\<alpha>\<close>. Beyond
the underlying locale, a corresponding type class is established which is
- interpreted logically as axiomatic type class @{cite "Wenzel:1997:TPHOL"}
+ interpreted logically as axiomatic type class \<^cite>\<open>"Wenzel:1997:TPHOL"\<close>
whose logical content are the assumptions of the locale. Thus, classes
provide the full generality of locales combined with the commodity of type
- classes (notably type-inference). See @{cite "isabelle-classes"} for a short
+ classes (notably type-inference). See \<^cite>\<open>"isabelle-classes"\<close> for a short
tutorial.
\<^rail>\<open>
@@ -983,7 +983,7 @@
\<^medskip>
Co-regularity is a very fundamental property of the order-sorted algebra of
types. For example, it entails principal types and most general unifiers,
- e.g.\ see @{cite "nipkow-prehofer"}.
+ e.g.\ see \<^cite>\<open>"nipkow-prehofer"\<close>.
\<close>
@@ -1009,7 +1009,7 @@
global constraints on all occurrences. E.g.\ \<open>d :: \<alpha> \<times> \<alpha>\<close> on the left-hand
side means that all corresponding occurrences on some right-hand side need
to be an instance of this, and general \<open>d :: \<alpha> \<times> \<beta>\<close> will be disallowed. Full
- details are given by Kun\v{c}ar @{cite "Kuncar:2015"}.
+ details are given by Kun\v{c}ar \<^cite>\<open>"Kuncar:2015"\<close>.
\<^medskip>
The \<^theory_text>\<open>consts\<close> command and the \<^theory_text>\<open>overloading\<close> target provide a convenient
@@ -1139,7 +1139,7 @@
exported to the global bootstrap environment of the ML process --- it has
a lasting effect that cannot be retracted. This allows ML evaluation
without a formal theory context, e.g. for command-line tools via @{tool
- process} @{cite "isabelle-system"}.
+ process} \<^cite>\<open>"isabelle-system"\<close>.
\<^descr> \<^theory_text>\<open>ML_prf\<close> is analogous to \<^theory_text>\<open>ML\<close> but works within a proof context.
Top-level ML bindings are stored within the proof context in a purely
@@ -1199,14 +1199,14 @@
debugging information. The global system option @{system_option_ref
ML_debugger} does the same when building a session image. It is also
possible use commands like \<^theory_text>\<open>ML_file_debug\<close> etc. The ML debugger is
- explained further in @{cite "isabelle-jedit"}.
+ explained further in \<^cite>\<open>"isabelle-jedit"\<close>.
\<^descr> @{attribute ML_exception_trace} indicates whether the ML run-time system
should print a detailed stack trace on exceptions. The result is dependent
on various ML compiler optimizations. The boundary for the exception trace
is the current Isar command transactions: it is occasionally better to
insert the combinator \<^ML>\<open>Runtime.exn_trace\<close> into ML code for debugging
- @{cite "isabelle-implementation"}, closer to the point where it actually
+ \<^cite>\<open>"isabelle-implementation"\<close>, closer to the point where it actually
happens.
\<^descr> @{attribute ML_exception_debugger} controls detailed exception trace via
@@ -1258,7 +1258,7 @@
\<^descr>[Exported files] are stored within the session database in
Isabelle/Scala. This allows to deliver artefacts to external tools, see
- also @{cite "isabelle-system"} for session \<^verbatim>\<open>ROOT\<close> declaration
+ also \<^cite>\<open>"isabelle-system"\<close> for session \<^verbatim>\<open>ROOT\<close> declaration
\<^theory_text>\<open>export_files\<close>, and @{tool build} option \<^verbatim>\<open>-e\<close>.
A notable example is the command @{command_ref export_code}
@@ -1323,7 +1323,7 @@
\<^descr> \<^theory_text>\<open>scala_build_generated_files paths (in thy)\<close> retrieves named generated
files as for \<^theory_text>\<open>export_generated_files\<close> and writes them into a temporary
directory, which is taken as starting point for build process of
- Isabelle/Scala/Java modules (see @{cite "isabelle-system"}). The
+ Isabelle/Scala/Java modules (see \<^cite>\<open>"isabelle-system"\<close>). The
corresponding @{path \<open>build.props\<close>} file is expected directly in the toplevel
directory, instead of @{path \<open>etc/build.props\<close>} for Isabelle system
components. These properties need to specify sources, resources, services
@@ -1356,8 +1356,7 @@
exports of \<^theory_text>\<open>export_files\<close> above.
\<^descr> \<^theory_text>\<open>external_file name\<close> declares the formal dependency on the given file
- name, such that the Isabelle build process knows about it (see also @{cite
- "isabelle-system"}). This is required for any files mentioned in
+ name, such that the Isabelle build process knows about it (see also \<^cite>\<open>"isabelle-system"\<close>). This is required for any files mentioned in
\<^theory_text>\<open>compile_generated_files / external_files\<close> above, in order to document
source dependencies properly. It is also possible to use \<^theory_text>\<open>external_file\<close>
alone, e.g.\ when other Isabelle/ML tools use \<^ML>\<open>File.read\<close>, without
--- a/src/Doc/JEdit/JEdit.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/JEdit/JEdit.thy Sun Jan 15 18:30:18 2023 +0100
@@ -10,16 +10,16 @@
text \<open>
Isabelle/jEdit is a Prover IDE that integrates \<^emph>\<open>parallel proof checking\<close>
- @{cite "Wenzel:2009" and "Wenzel:2013:ITP"} with \<^emph>\<open>asynchronous user
- interaction\<close> @{cite "Wenzel:2010" and "Wenzel:2012:UITP-EPTCS" and
- "Wenzel:2014:ITP-PIDE" and "Wenzel:2014:UITP"}, based on a document-oriented
- approach to \<^emph>\<open>continuous proof processing\<close> @{cite "Wenzel:2011:CICM" and
- "Wenzel:2012" and "Wenzel:2018:FIDE" and "Wenzel:2019:MKM"}. Many concepts
+ \<^cite>\<open>"Wenzel:2009" and "Wenzel:2013:ITP"\<close> with \<^emph>\<open>asynchronous user
+ interaction\<close> \<^cite>\<open>"Wenzel:2010" and "Wenzel:2012:UITP-EPTCS" and
+ "Wenzel:2014:ITP-PIDE" and "Wenzel:2014:UITP"\<close>, based on a document-oriented
+ approach to \<^emph>\<open>continuous proof processing\<close> \<^cite>\<open>"Wenzel:2011:CICM" and
+ "Wenzel:2012" and "Wenzel:2018:FIDE" and "Wenzel:2019:MKM"\<close>. Many concepts
and system components are fit together in order to make this work. The main
building blocks are as follows.
\<^descr>[Isabelle/ML] is the implementation and extension language of Isabelle,
- see also @{cite "isabelle-implementation"}. It is integrated into the
+ see also \<^cite>\<open>"isabelle-implementation"\<close>. It is integrated into the
logical context of Isabelle/Isar and allows to manipulate logical entities
directly. Arbitrary add-on tools may be implemented for object-logics such
as Isabelle/HOL.
@@ -84,7 +84,7 @@
The options allow to specify a logic session name, but the same selector is
also accessible in the \<^emph>\<open>Theories\<close> panel (\secref{sec:theories}). After
startup of the Isabelle plugin, the selected logic session image is provided
- automatically by the Isabelle build tool @{cite "isabelle-system"}: if it is
+ automatically by the Isabelle build tool \<^cite>\<open>"isabelle-system"\<close>: if it is
absent or outdated wrt.\ its sources, the build process updates it within
the running text editor. Prover IDE functionality is fully activated after
successful termination of the build process. A failure may require changing
@@ -171,7 +171,7 @@
Isabelle system options are managed by Isabelle/Scala and changes are stored
in \<^path>\<open>$ISABELLE_HOME_USER/etc/preferences\<close>, independently of
- other jEdit properties. See also @{cite "isabelle-system"}, especially the
+ other jEdit properties. See also \<^cite>\<open>"isabelle-system"\<close>, especially the
coverage of sessions and command-line tools like @{tool build} or @{tool
options}.
@@ -182,8 +182,7 @@
Isabelle\<close> in jEdit provides a view on a subset of Isabelle system options.
Note that some of these options affect general parameters that are relevant
outside Isabelle/jEdit as well, e.g.\ @{system_option threads} or
- @{system_option parallel_proofs} for the Isabelle build tool @{cite
- "isabelle-system"}, but it is possible to use the settings variable
+ @{system_option parallel_proofs} for the Isabelle build tool \<^cite>\<open>"isabelle-system"\<close>, but it is possible to use the settings variable
@{setting ISABELLE_BUILD_OPTIONS} to change defaults for batch builds
without affecting the Prover IDE.
@@ -253,8 +252,7 @@
The \<^verbatim>\<open>-l\<close> option specifies the session name of the logic image to be used
for proof processing. Additional session root directories may be included
- via option \<^verbatim>\<open>-d\<close> to augment the session name space (see also @{cite
- "isabelle-system"}). By default, the specified image is checked and built on
+ via option \<^verbatim>\<open>-d\<close> to augment the session name space (see also \<^cite>\<open>"isabelle-system"\<close>). By default, the specified image is checked and built on
demand, but option \<^verbatim>\<open>-n\<close> bypasses the implicit build process for the
selected session image. Options \<^verbatim>\<open>-s\<close> and \<^verbatim>\<open>-u\<close> override the default system
option @{system_option system_heaps}: this determines where to store the
@@ -277,7 +275,7 @@
The \<^verbatim>\<open>-J\<close> and \<^verbatim>\<open>-j\<close> options pass additional low-level options to the JVM or
jEdit, respectively. The defaults are provided by the Isabelle settings
- environment @{cite "isabelle-system"}, but note that these only work for the
+ environment \<^cite>\<open>"isabelle-system"\<close>, but note that these only work for the
command-line tool described here, and not the desktop application.
The \<^verbatim>\<open>-D\<close> option allows to define JVM system properties; this is passed
@@ -454,7 +452,7 @@
standards.\<^footnote>\<open>Raw Unicode characters within formal sources compromise
portability and reliability in the face of changing interpretation of
special features of Unicode, such as Combining Characters or Bi-directional
- Text.\<close> See @{cite "Wenzel:2011:CICM"}.
+ Text.\<close> See \<^cite>\<open>"Wenzel:2011:CICM"\<close>.
For the prover back-end, formal text consists of ASCII characters that are
grouped according to some simple rules, e.g.\ as plain ``\<^verbatim>\<open>a\<close>'' or symbolic
@@ -464,7 +462,7 @@
in \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> and may be augmented by the user in
\<^path>\<open>$ISABELLE_HOME_USER/etc/symbols\<close>.
- The appendix of @{cite "isabelle-isar-ref"} gives an overview of the
+ The appendix of \<^cite>\<open>"isabelle-isar-ref"\<close> gives an overview of the
standard interpretation of finitely many symbols from the infinite
collection. Uninterpreted symbols are displayed literally, e.g.\
``\<^verbatim>\<open>\<foobar>\<close>''. Overlap of Unicode characters used in symbol
@@ -718,7 +716,7 @@
according to a snapshot of the document model. The file browser is \<^emph>\<open>not\<close>
updated continuously when the PIDE document changes: the reload operation
needs to be used explicitly. A notable example for exports is the command
- @{command_ref export_code} @{cite "isabelle-isar-ref"}.
+ @{command_ref export_code} \<^cite>\<open>"isabelle-isar-ref"\<close>.
\<^item> URL \<^verbatim>\<open>isabelle-session:\<close> or action @{action_def
"isabelle-session-browser"} show the structure of session chapters and
@@ -789,7 +787,7 @@
\<^medskip>
Isabelle/ML files are structured according to semi-formal comments that are
- explained in @{cite "isabelle-implementation"}. This outline is turned into
+ explained in \<^cite>\<open>"isabelle-implementation"\<close>. This outline is turned into
a tree-view by default, by using the \<^verbatim>\<open>isabelle-ml\<close> parser. There is also a
folding mode of the same name, for hierarchic text folds within ML files.
@@ -844,12 +842,11 @@
nodes in two dimensions:
\<^enum> via \<^bold>\<open>theory imports\<close> that are specified in the \<^emph>\<open>theory header\<close> using
- concrete syntax of the @{command_ref theory} command @{cite
- "isabelle-isar-ref"};
+ concrete syntax of the @{command_ref theory} command \<^cite>\<open>"isabelle-isar-ref"\<close>;
\<^enum> via \<^bold>\<open>auxiliary files\<close> that are included into a theory by \<^emph>\<open>load
commands\<close>, notably @{command_ref ML_file} and @{command_ref SML_file}
- @{cite "isabelle-isar-ref"}.
+ \<^cite>\<open>"isabelle-isar-ref"\<close>.
In any case, source files are managed by the PIDE infrastructure: the
physical file-system only plays a subordinate role. The relevant version of
@@ -924,7 +921,7 @@
text \<open>
Special load commands like @{command_ref ML_file} and @{command_ref
- SML_file} @{cite "isabelle-isar-ref"} refer to auxiliary files within some
+ SML_file} \<^cite>\<open>"isabelle-isar-ref"\<close> refer to auxiliary files within some
theory. Conceptually, the file argument of the command extends the theory
source by the content of the file, but its editor buffer may be loaded~/
changed~/ saved separately. The PIDE document model propagates changes of
@@ -1182,8 +1179,7 @@
'solves' | 'simp' ':' @{syntax term} | @{syntax term})
\<close>
- See also the Isar command @{command_ref find_theorems} in @{cite
- "isabelle-isar-ref"}.
+ See also the Isar command @{command_ref find_theorems} in \<^cite>\<open>"isabelle-isar-ref"\<close>.
\<close>
@@ -1199,8 +1195,7 @@
('name' ':' @{syntax name} | 'strict' ':' @{syntax type} | @{syntax type})
\<close>
- See also the Isar command @{command_ref find_consts} in @{cite
- "isabelle-isar-ref"}.
+ See also the Isar command @{command_ref find_consts} in \<^cite>\<open>"isabelle-isar-ref"\<close>.
\<close>
@@ -1210,8 +1205,7 @@
The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Print Context\<close> mode prints information from the
theory or proof context, or proof state. See also the Isar commands
@{command_ref print_context}, @{command_ref print_cases}, @{command_ref
- print_term_bindings}, @{command_ref print_theorems}, described in @{cite
- "isabelle-isar-ref"}.
+ print_term_bindings}, @{command_ref print_theorems}, described in \<^cite>\<open>"isabelle-isar-ref"\<close>.
\<close>
@@ -1437,7 +1431,7 @@
text \<open>
The theory header syntax supports abbreviations via the \<^theory_text>\<open>abbrevs\<close> keyword
- @{cite "isabelle-isar-ref"}. This is a slight generalization of built-in
+ \<^cite>\<open>"isabelle-isar-ref"\<close>. This is a slight generalization of built-in
templates and abbreviations for Isabelle symbols, as explained above.
Examples may be found in the Isabelle sources, by searching for
``\<^verbatim>\<open>abbrevs\<close>'' in \<^verbatim>\<open>*.thy\<close> files.
@@ -1757,8 +1751,7 @@
\<^item> @{system_option_ref auto_methods} controls automatic use of a combination
of standard proof methods (@{method auto}, @{method simp}, @{method blast},
- etc.). This corresponds to the Isar command @{command_ref "try0"} @{cite
- "isabelle-isar-ref"}.
+ etc.). This corresponds to the Isar command @{command_ref "try0"} \<^cite>\<open>"isabelle-isar-ref"\<close>.
The tool is disabled by default, since unparameterized invocation of
standard proof methods often consumes substantial CPU resources without
@@ -1766,7 +1759,7 @@
\<^item> @{system_option_ref auto_nitpick} controls a slightly reduced version of
@{command_ref nitpick}, which tests for counterexamples using first-order
- relational logic. See also the Nitpick manual @{cite "isabelle-nitpick"}.
+ relational logic. See also the Nitpick manual \<^cite>\<open>"isabelle-nitpick"\<close>.
This tool is disabled by default, due to the extra overhead of invoking an
external Java process for each attempt to disprove a subgoal.
@@ -1780,8 +1773,7 @@
\<^item> @{system_option_ref auto_sledgehammer} controls a significantly reduced
version of @{command_ref sledgehammer}, which attempts to prove a subgoal
- using external automatic provers. See also the Sledgehammer manual @{cite
- "isabelle-sledgehammer"}.
+ using external automatic provers. See also the Sledgehammer manual \<^cite>\<open>"isabelle-sledgehammer"\<close>.
This tool is disabled by default, due to the relatively heavy nature of
Sledgehammer.
@@ -1853,7 +1845,7 @@
text \<open>
The ultimate purpose of Isabelle is to produce nicely rendered documents
with the Isabelle document preparation system, which is based on {\LaTeX};
- see also @{cite "isabelle-system" and "isabelle-isar-ref"}. Isabelle/jEdit
+ see also \<^cite>\<open>"isabelle-system" and "isabelle-isar-ref"\<close>. Isabelle/jEdit
provides some additional support for document editing.
\<close>
@@ -1912,12 +1904,10 @@
text \<open>
Citations are managed by {\LaTeX} and Bib{\TeX} in \<^verbatim>\<open>.bib\<close> files. The
- Isabelle session build process and the @{tool document} tool @{cite
- "isabelle-system"} are smart enough to assemble the result, based on the
+ Isabelle session build process and the @{tool document} tool \<^cite>\<open>"isabelle-system"\<close> are smart enough to assemble the result, based on the
session directory layout.
- The document antiquotation \<open>@{cite}\<close> is described in @{cite
- "isabelle-isar-ref"}. Within the Prover IDE it provides semantic markup for
+ The document antiquotation \<open>@{cite}\<close> is described in \<^cite>\<open>"isabelle-isar-ref"\<close>. Within the Prover IDE it provides semantic markup for
tooltips, hyperlinks, and completion for Bib{\TeX} database entries.
Isabelle/jEdit does \<^emph>\<open>not\<close> know about the actual Bib{\TeX} environment used
in {\LaTeX} batch-mode, but it can take citations from those \<^verbatim>\<open>.bib\<close> files
--- a/src/Doc/Locales/Examples.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Locales/Examples.thy Sun Jan 15 18:30:18 2023 +0100
@@ -292,7 +292,7 @@
exception of the context elements \isakeyword{constrains} and
\isakeyword{defines}, which are provided for backward
compatibility. See the Isabelle/Isar Reference
- Manual @{cite IsarRef} for full documentation.\<close>
+ Manual \<^cite>\<open>IsarRef\<close> for full documentation.\<close>
section \<open>Import \label{sec:import}\<close>
@@ -757,7 +757,7 @@
The sublocale relation is transitive --- that is, propagation takes
effect along chains of sublocales. Even cycles in the sublocale relation are
supported, as long as these cycles do not lead to infinite chains.
- Details are discussed in the technical report @{cite Ballarin2006a}.
+ Details are discussed in the technical report \<^cite>\<open>Ballarin2006a\<close>.
See also Section~\ref{sec:infinite-chains} of this tutorial.\<close>
end
--- a/src/Doc/Locales/Examples3.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Locales/Examples3.thy Sun Jan 15 18:30:18 2023 +0100
@@ -486,13 +486,13 @@
text \<open>More information on locales and their interpretation is
available. For the locale hierarchy of import and interpretation
- dependencies see~@{cite Ballarin2006a}; interpretations in theories
- and proofs are covered in~@{cite Ballarin2006b}. In the latter, I
+ dependencies see~\<^cite>\<open>Ballarin2006a\<close>; interpretations in theories
+ and proofs are covered in~\<^cite>\<open>Ballarin2006b\<close>. In the latter, I
show how interpretation in proofs enables to reason about families
of algebraic structures, which cannot be expressed with locales
directly.
- Haftmann and Wenzel~@{cite HaftmannWenzel2007} overcome a restriction
+ Haftmann and Wenzel~\<^cite>\<open>HaftmannWenzel2007\<close> overcome a restriction
of axiomatic type classes through a combination with locale
interpretation. The result is a Haskell-style class system with a
facility to generate ML and Haskell code. Classes are sufficient for
@@ -504,14 +504,14 @@
The locales reimplementation for Isabelle 2009 provides, among other
improvements, a clean integration with Isabelle/Isar's local theory
mechanisms, which are described in another paper by Haftmann and
- Wenzel~@{cite HaftmannWenzel2009}.
+ Wenzel~\<^cite>\<open>HaftmannWenzel2009\<close>.
- The original work of Kammüller on locales~@{cite KammullerEtAl1999}
+ The original work of Kammüller on locales~\<^cite>\<open>KammullerEtAl1999\<close>
may be of interest from a historical perspective. My previous
- report on locales and locale expressions~@{cite Ballarin2004a}
+ report on locales and locale expressions~\<^cite>\<open>Ballarin2004a\<close>
describes a simpler form of expressions than available now and is
outdated. The mathematical background on orders and lattices is
- taken from Jacobson's textbook on algebra~@{cite \<open>Chapter~8\<close> Jacobson1985}.
+ taken from Jacobson's textbook on algebra~\<^cite>\<open>\<open>Chapter~8\<close> in Jacobson1985\<close>.
The sources of this tutorial, which include all proofs, are
available with the Isabelle distribution at
--- a/src/Doc/Logics_ZF/ZF_Isar.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Logics_ZF/ZF_Isar.thy Sun Jan 15 18:30:18 2023 +0100
@@ -93,7 +93,7 @@
hints: @{syntax (ZF) "monos"}? @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
\<close>
- See @{cite "isabelle-ZF"} for further information on inductive
+ See \<^cite>\<open>"isabelle-ZF"\<close> for further information on inductive
definitions in ZF, but note that this covers the old-style theory
format.
\<close>
--- a/src/Doc/Prog_Prove/Isar.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Prog_Prove/Isar.thy Sun Jan 15 18:30:18 2023 +0100
@@ -504,7 +504,7 @@
Therefore the \isacom{also} hidden in \isacom{finally} sets \<open>calculation\<close>
to \<open>t\<^sub>1 < t\<^sub>4\<close> and the final ``\texttt{.}'' succeeds.
-For more information on this style of proof see @{cite "BauerW-TPHOLs01"}.
+For more information on this style of proof see \<^cite>\<open>"BauerW-TPHOLs01"\<close>.
\fi
\section{Streamlining Proofs}
--- a/src/Doc/Prog_Prove/Logic.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Prog_Prove/Logic.thy Sun Jan 15 18:30:18 2023 +0100
@@ -141,7 +141,7 @@
@{thm image_def}\index{$IMP042@\<^term>\<open>f ` A\<close>} & is the image of a function over a set
\end{tabular}
\end{center}
-See @{cite "Nipkow-Main"} for the wealth of further predefined functions in theory
+See \<^cite>\<open>"Nipkow-Main"\<close> for the wealth of further predefined functions in theory
\<^theory>\<open>Main\<close>.
@@ -399,7 +399,7 @@
{\mbox{\<open>?P = ?Q\<close>}}
\]
These rules are part of the logical system of \concept{natural deduction}
-(e.g., @{cite HuthRyan}). Although we intentionally de-emphasize the basic rules
+(e.g., \<^cite>\<open>HuthRyan\<close>). Although we intentionally de-emphasize the basic rules
of logic in favour of automatic proof methods that allow you to take bigger
steps, these rules are helpful in locating where and why automation fails.
When applied backwards, these rules decompose the goal:
@@ -483,7 +483,7 @@
%
%Command \isacom{find{\isacharunderscorekeyword}theorems} searches for specific theorems in the current
%theory. Search criteria include pattern matching on terms and on names.
-%For details see the Isabelle/Isar Reference Manual~@{cite IsarRef}.
+%For details see the Isabelle/Isar Reference Manual~\<^cite>\<open>IsarRef\<close>.
%\bigskip
\begin{warn}
--- a/src/Doc/Prog_Prove/Types_and_funs.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy Sun Jan 15 18:30:18 2023 +0100
@@ -147,7 +147,7 @@
fixed argument position decreases in size with each recursive call. The size
is measured as the number of constructors (excluding 0-ary ones, e.g., \<open>Nil\<close>). Lexicographic combinations are also recognized. In more complicated
situations, the user may have to prove termination by hand. For details
-see~@{cite Krauss}.
+see~\<^cite>\<open>Krauss\<close>.
Functions defined with \isacom{fun} come with their own induction schema
that mirrors the recursion schema and is derived from the termination
--- a/src/Doc/Sugar/Sugar.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Sugar/Sugar.thy Sun Jan 15 18:30:18 2023 +0100
@@ -18,7 +18,7 @@
@{thm[display,mode=latex_sum] sum_Suc_diff[no_vars]}
No typos, no omissions, no sweat.
If you have not experienced that joy, read Chapter 4, \emph{Presenting
-Theories}, @{cite LNCS2283} first.
+Theories}, \<^cite>\<open>LNCS2283\<close> first.
If you have mastered the art of Isabelle's \emph{antiquotations},
i.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity
@@ -234,7 +234,7 @@
\subsection{Inference rules}
To print theorems as inference rules you need to include Didier
-R\'emy's \texttt{mathpartir} package~@{cite mathpartir}
+R\'emy's \texttt{mathpartir} package~\<^cite>\<open>mathpartir\<close>
for typesetting inference rules in your \LaTeX\ file.
Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces
--- a/src/Doc/System/Environment.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/System/Environment.thy Sun Jan 15 18:30:18 2023 +0100
@@ -8,10 +8,8 @@
text \<open>
This manual describes Isabelle together with related tools as seen from a
- system oriented view. See also the \<^emph>\<open>Isabelle/Isar Reference Manual\<close> @{cite
- "isabelle-isar-ref"} for the actual Isabelle input language and related
- concepts, and \<^emph>\<open>The Isabelle/Isar Implementation Manual\<close> @{cite
- "isabelle-implementation"} for the main concepts of the underlying
+ system oriented view. See also the \<^emph>\<open>Isabelle/Isar Reference Manual\<close> \<^cite>\<open>"isabelle-isar-ref"\<close> for the actual Isabelle input language and related
+ concepts, and \<^emph>\<open>The Isabelle/Isar Implementation Manual\<close> \<^cite>\<open>"isabelle-implementation"\<close> for the main concepts of the underlying
implementation in Isabelle/ML.
\<close>
--- a/src/Doc/System/Scala.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/System/Scala.thy Sun Jan 15 18:30:18 2023 +0100
@@ -13,7 +13,7 @@
\<^item> Isabelle/ML is for \<^emph>\<open>mathematics\<close>, to develop tools within the context
of symbolic logic, e.g.\ for constructing proofs or defining
domain-specific formal languages. See the \<^emph>\<open>Isabelle/Isar implementation
- manual\<close> @{cite "isabelle-implementation"} for more details.
+ manual\<close> \<^cite>\<open>"isabelle-implementation"\<close> for more details.
\<^item> Isabelle/Scala is for \<^emph>\<open>physics\<close>, to connect with the world of systems
and services, including editors and IDE frameworks.
@@ -27,7 +27,7 @@
(\secref{sec:scala-functions}) via the PIDE protocol: execution happens
within the running Java process underlying Isabelle/Scala.
- \<^item> The \<^verbatim>\<open>Console/Scala\<close> plugin of Isabelle/jEdit @{cite "isabelle-jedit"}
+ \<^item> The \<^verbatim>\<open>Console/Scala\<close> plugin of Isabelle/jEdit \<^cite>\<open>"isabelle-jedit"\<close>
operates on the running Java application, using the Scala
read-eval-print-loop (REPL).
--- a/src/Doc/System/Server.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/System/Server.thy Sun Jan 15 18:30:18 2023 +0100
@@ -463,8 +463,7 @@
string, id?: long}\<close> describes a source position within Isabelle text. Only
the \<open>line\<close> and \<open>file\<close> fields make immediate sense to external programs.
Detailed \<open>offset\<close> and \<open>end_offset\<close> positions are counted according to
- Isabelle symbols, see \<^ML_type>\<open>Symbol.symbol\<close> in Isabelle/ML @{cite
- "isabelle-implementation"}. The position \<open>id\<close> belongs to the representation
+ Isabelle symbols, see \<^ML_type>\<open>Symbol.symbol\<close> in Isabelle/ML \<^cite>\<open>"isabelle-implementation"\<close>. The position \<open>id\<close> belongs to the representation
of command transactions in the Isabelle/PIDE protocol: it normally does not
occur in externalized positions.
@@ -732,7 +731,7 @@
text \<open>
The asynchronous notifications of command \<^verbatim>\<open>session_build\<close> mainly serve as
progress indicator: the output resembles that of the session build window of
- Isabelle/jEdit after startup @{cite "isabelle-jedit"}.
+ Isabelle/jEdit after startup \<^cite>\<open>"isabelle-jedit"\<close>.
For the client it is usually sufficient to print the messages in plain text,
but note that \<open>theory_progress\<close> also reveals formal \<open>theory\<close> and
@@ -1012,7 +1011,7 @@
\<^item> \<open>theory_name\<close>: the logical theory name;
\<^item> \<open>status\<close>: the overall node status, e.g.\ see the visualization in the
- \<open>Theories\<close> panel of Isabelle/jEdit @{cite "isabelle-jedit"};
+ \<open>Theories\<close> panel of Isabelle/jEdit \<^cite>\<open>"isabelle-jedit"\<close>;
\<^item> \<open>messages\<close>: the main bulk of prover messages produced in this theory
(with kind \<^verbatim>\<open>writeln\<close>, \<^verbatim>\<open>warning\<close>, \<^verbatim>\<open>error\<close>).
--- a/src/Doc/System/Sessions.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/System/Sessions.thy Sun Jan 15 18:30:18 2023 +0100
@@ -36,7 +36,7 @@
additional project directories given by the user.
The ROOT file format follows the lexical conventions of the \<^emph>\<open>outer syntax\<close>
- of Isabelle/Isar, see also @{cite "isabelle-isar-ref"}. This defines common
+ of Isabelle/Isar, see also \<^cite>\<open>"isabelle-isar-ref"\<close>. This defines common
forms like identifiers, names, quoted strings, verbatim text, nested
comments etc. The grammar for @{syntax chapter_def}, @{syntax chapter_entry}
and @{syntax session_entry} is given as syntax diagram below. Each ROOT file
@@ -45,7 +45,7 @@
chapter is ``\<open>Unsorted\<close>''. Chapter definitions, which are optional, allow to
associate additional information.
- Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple editing mode
+ Isabelle/jEdit \<^cite>\<open>"isabelle-jedit"\<close> includes a simple editing mode
\<^verbatim>\<open>isabelle-root\<close> for session ROOT files, which is enabled by default for any
file of that name.
@@ -192,7 +192,7 @@
tools require global configuration during system startup. An empty list of
\<open>patterns\<close> defaults to \<^verbatim>\<open>"*:classpath/*.jar"\<close>, which fits to the naming
convention of JAR modules produced by the Isabelle/Isar command
- \<^theory_text>\<open>scala_build_generated_files\<close> @{cite "isabelle-isar-ref"}.
+ \<^theory_text>\<open>scala_build_generated_files\<close> \<^cite>\<open>"isabelle-isar-ref"\<close>.
\<close>
@@ -211,7 +211,7 @@
text \<open>
See \<^file>\<open>~~/etc/options\<close> for the main defaults provided by the Isabelle
- distribution. Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple
+ distribution. Isabelle/jEdit \<^cite>\<open>"isabelle-jedit"\<close> includes a simple
editing mode \<^verbatim>\<open>isabelle-options\<close> for this file-format.
The following options are particularly relevant to build Isabelle sessions,
--- a/src/Doc/Tutorial/Advanced/simp2.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Tutorial/Advanced/simp2.thy Sun Jan 15 18:30:18 2023 +0100
@@ -122,7 +122,7 @@
rewrite rules. This is not quite true. For reasons of feasibility,
the simplifier expects the
left-hand side of each rule to be a so-called \emph{higher-order
-pattern}~@{cite "nipkow-patterns"}\indexbold{patterns!higher-order}.
+pattern}~\<^cite>\<open>"nipkow-patterns"\<close>\indexbold{patterns!higher-order}.
This restricts where
unknowns may occur. Higher-order patterns are terms in $\beta$-normal
form. (This means there are no subterms of the form $(\lambda x. M)(N)$.)
--- a/src/Doc/Tutorial/CTL/Base.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Tutorial/CTL/Base.thy Sun Jan 15 18:30:18 2023 +0100
@@ -7,7 +7,7 @@
Computation Tree Logic (CTL), a temporal logic.
Model checking is a popular technique for the verification of finite
state systems (implementations) with respect to temporal logic formulae
-(specifications) @{cite "ClarkeGP-book" and "Huth-Ryan-book"}. Its foundations are set theoretic
+(specifications) \<^cite>\<open>"ClarkeGP-book" and "Huth-Ryan-book"\<close>. Its foundations are set theoretic
and this section will explore them in HOL\@. This is done in two steps. First
we consider a simple modal logic called propositional dynamic
logic (PDL)\@. We then proceed to the temporal logic CTL, which is
--- a/src/Doc/Tutorial/CTL/CTL.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Tutorial/CTL/CTL.thy Sun Jan 15 18:30:18 2023 +0100
@@ -361,7 +361,7 @@
%{text[display]"| EU formula formula E[_ U _]"}
%which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.
\end{exercise}
-For more CTL exercises see, for example, Huth and Ryan @{cite "Huth-Ryan-book"}.
+For more CTL exercises see, for example, Huth and Ryan \<^cite>\<open>"Huth-Ryan-book"\<close>.
\<close>
(*<*)
@@ -439,7 +439,7 @@
our model checkers. It is clear that if all sets are finite, they can be
represented as lists and the usual set operations are easily
implemented. Only \<^const>\<open>lfp\<close> requires a little thought. Fortunately, theory
-\<open>While_Combinator\<close> in the Library~@{cite "HOL-Library"} provides a
+\<open>While_Combinator\<close> in the Library~\<^cite>\<open>"HOL-Library"\<close> provides a
theorem stating that in the case of finite sets and a monotone
function~\<^term>\<open>F\<close>, the value of \mbox{\<^term>\<open>lfp F\<close>} can be computed by
iterated application of \<^term>\<open>F\<close> to~\<^term>\<open>{}\<close> until a fixed point is
--- a/src/Doc/Tutorial/CTL/PDL.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Tutorial/CTL/PDL.thy Sun Jan 15 18:30:18 2023 +0100
@@ -8,7 +8,7 @@
connectives \<open>AX\<close> and \<open>EF\<close>\@. Since formulae are essentially
syntax trees, they are naturally modelled as a datatype:%
\footnote{The customary definition of PDL
-@{cite "HarelKT-DL"} looks quite different from ours, but the two are easily
+\<^cite>\<open>"HarelKT-DL"\<close> looks quite different from ours, but the two are easily
shown to be equivalent.}
\<close>
--- a/src/Doc/Tutorial/Datatype/Nested.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Tutorial/Datatype/Nested.thy Sun Jan 15 18:30:18 2023 +0100
@@ -149,7 +149,7 @@
instead. Simple uses of \isacommand{fun} are described in
\S\ref{sec:fun} below. Advanced applications, including functions
over nested datatypes like \<open>term\<close>, are discussed in a
-separate tutorial~@{cite "isabelle-function"}.
+separate tutorial~\<^cite>\<open>"isabelle-function"\<close>.
Of course, you may also combine mutual and nested recursion of datatypes. For example,
constructor \<open>Sum\<close> in \S\ref{sec:datatype-mut-rec} could take a list of
--- a/src/Doc/Tutorial/Documents/Documents.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Tutorial/Documents/Documents.thy Sun Jan 15 18:30:18 2023 +0100
@@ -11,7 +11,7 @@
for the parser and output templates for the pretty printer.
In full generality, parser and pretty printer configuration is a
- subtle affair~@{cite "isabelle-isar-ref"}. Your syntax specifications need
+ subtle affair~\<^cite>\<open>"isabelle-isar-ref"\<close>. Your syntax specifications need
to interact properly with the existing setup of Isabelle/Pure and
Isabelle/HOL\@. To avoid creating ambiguities with existing
elements, it is particularly important to give new syntactic
@@ -106,7 +106,7 @@
display the \verb,\,\verb,<forall>, symbol as~\<open>\<forall>\<close>.
A list of standard Isabelle symbols is given in
- @{cite "isabelle-isar-ref"}. You may introduce your own
+ \<^cite>\<open>"isabelle-isar-ref"\<close>. You may introduce your own
interpretation of further symbols by configuring the appropriate
front-end tool accordingly, e.g.\ by defining certain {\LaTeX}
macros (see also \S\ref{sec:doc-prep-symbols}). There are also a
@@ -146,7 +146,7 @@
text \<open>
It is possible to provide alternative syntax forms
- through the \bfindex{print mode} concept~@{cite "isabelle-isar-ref"}. By
+ through the \bfindex{print mode} concept~\<^cite>\<open>"isabelle-isar-ref"\<close>. By
convention, the mode of ``$xsymbols$'' is enabled whenever
Proof~General's X-Symbol mode or {\LaTeX} output is active. Now
consider the following hybrid declaration of \<open>xor\<close>:
@@ -180,7 +180,7 @@
text \<open>
Prefix syntax annotations\index{prefix annotation} are another form
- of mixfixes @{cite "isabelle-isar-ref"}, without any template arguments or
+ of mixfixes \<^cite>\<open>"isabelle-isar-ref"\<close>, without any template arguments or
priorities --- just some literal syntax. The following example
associates common symbols with the constructors of a datatype.
\<close>
@@ -254,7 +254,7 @@
Abbreviations are a simplified form of the general concept of
\emph{syntax translations}; even heavier transformations may be
-written in ML @{cite "isabelle-isar-ref"}.
+written in ML \<^cite>\<open>"isabelle-isar-ref"\<close>.
\<close>
@@ -342,7 +342,7 @@
setup) and \texttt{isabelle build} (to run sessions as specified in
the corresponding \texttt{ROOT} file). These Isabelle tools are
described in further detail in the \emph{Isabelle System Manual}
- @{cite "isabelle-system"}.
+ \<^cite>\<open>"isabelle-system"\<close>.
For example, a new session \texttt{MySession} (with document
preparation) may be produced as follows:
@@ -403,7 +403,7 @@
\texttt{MySession/document} directory as well. In particular,
adding a file named \texttt{root.bib} causes an automatic run of
\texttt{bibtex} to process a bibliographic database; see also
- \texttt{isabelle document} @{cite "isabelle-system"}.
+ \texttt{isabelle document} \<^cite>\<open>"isabelle-system"\<close>.
\medskip Any failure of the document preparation phase in an
Isabelle batch session leaves the generated sources in their target
@@ -473,7 +473,7 @@
theory or proof context (\bfindex{text blocks}).
\medskip Marginal comments are part of each command's concrete
- syntax @{cite "isabelle-isar-ref"}; the common form is ``\verb,--,~$text$''
+ syntax \<^cite>\<open>"isabelle-isar-ref"\<close>; the common form is ``\verb,--,~$text$''
where $text$ is delimited by \verb,",\<open>\<dots>\<close>\verb,", or
\verb,{,\verb,*,~\<open>\<dots>\<close>~\verb,*,\verb,}, as before. Multiple
marginal comments may be given at the same time. Here is a simple
@@ -552,7 +552,7 @@
same types as they have in the main goal statement.
\medskip Several further kinds of antiquotations and options are
- available @{cite "isabelle-isar-ref"}. Here are a few commonly used
+ available \<^cite>\<open>"isabelle-isar-ref"\<close>. Here are a few commonly used
combinations:
\medskip
@@ -600,7 +600,7 @@
straightforward generalization of ASCII characters. While Isabelle
does not impose any interpretation of the infinite collection of
named symbols, {\LaTeX} documents use canonical glyphs for certain
- standard symbols @{cite "isabelle-isar-ref"}.
+ standard symbols \<^cite>\<open>"isabelle-isar-ref"\<close>.
The {\LaTeX} code produced from Isabelle text follows a simple
scheme. You can tune the final appearance by redefining certain
@@ -690,7 +690,7 @@
preparation system allows the user to specify how to interpret a
tagged region, in order to keep, drop, or fold the corresponding
parts of the document. See the \emph{Isabelle System Manual}
- @{cite "isabelle-system"} for further details, especially on
+ \<^cite>\<open>"isabelle-system"\<close> for further details, especially on
\texttt{isabelle build} and \texttt{isabelle document}.
Ignored material is specified by delimiting the original formal
--- a/src/Doc/Tutorial/Fun/fun0.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Tutorial/Fun/fun0.thy Sun Jan 15 18:30:18 2023 +0100
@@ -96,7 +96,7 @@
text\<open>The order of arguments has no influence on whether
\isacommand{fun} can prove termination of a function. For more details
-see elsewhere~@{cite bulwahnKN07}.
+see elsewhere~\<^cite>\<open>bulwahnKN07\<close>.
\subsection{Simplification}
\label{sec:fun-simplification}
--- a/src/Doc/Tutorial/Inductive/AB.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Tutorial/Inductive/AB.thy Sun Jan 15 18:30:18 2023 +0100
@@ -17,7 +17,7 @@
B &\to& b S \mid a B B \nonumber
\end{eqnarray}
At the end we say a few words about the relationship between
-the original proof @{cite \<open>p.\ts81\<close> HopcroftUllman} and our formal version.
+the original proof \<^cite>\<open>\<open>p.\ts81\<close> in HopcroftUllman\<close> and our formal version.
We start by fixing the alphabet, which consists only of \<^term>\<open>a\<close>'s
and~\<^term>\<open>b\<close>'s:
@@ -278,7 +278,7 @@
text\<open>
We conclude this section with a comparison of our proof with
Hopcroft\index{Hopcroft, J. E.} and Ullman's\index{Ullman, J. D.}
-@{cite \<open>p.\ts81\<close> HopcroftUllman}.
+\<^cite>\<open>\<open>p.\ts81\<close> in HopcroftUllman\<close>.
For a start, the textbook
grammar, for no good reason, excludes the empty word, thus complicating
matters just a little bit: they have 8 instead of our 7 productions.
--- a/src/Doc/Tutorial/Protocol/NS_Public.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Tutorial/Protocol/NS_Public.thy Sun Jan 15 18:30:18 2023 +0100
@@ -381,8 +381,8 @@
\medskip
Detailed information on this protocol verification technique can be found
-elsewhere~@{cite "paulson-jcs"}, including proofs of an Internet
-protocol~@{cite "paulson-tls"}. We must stress that the protocol discussed
+elsewhere~\<^cite>\<open>"paulson-jcs"\<close>, including proofs of an Internet
+protocol~\<^cite>\<open>"paulson-tls"\<close>. We must stress that the protocol discussed
in this chapter is trivial. There are only three messages; no keys are
exchanged; we merely have to prove that encrypted data remains secret.
Real world protocols are much longer and distribute many secrets to their
@@ -391,7 +391,7 @@
been used to encrypt other sensitive information, there may be cascading
losses. We may still be able to establish a bound on the losses and to
prove that other protocol runs function
-correctly~@{cite "paulson-yahalom"}. Proofs of real-world protocols follow
+correctly~\<^cite>\<open>"paulson-yahalom"\<close>. Proofs of real-world protocols follow
the strategy illustrated above, but the subgoals can
be much bigger and there are more of them.
\index{protocols!security|)}
--- a/src/Doc/Tutorial/Types/Axioms.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Tutorial/Types/Axioms.thy Sun Jan 15 18:30:18 2023 +0100
@@ -8,7 +8,7 @@
\begin{warn}
Proofs in this section use structured \emph{Isar} proofs, which are not
-covered in this tutorial; but see @{cite "Nipkow-TYPES02"}.%
+covered in this tutorial; but see \<^cite>\<open>"Nipkow-TYPES02"\<close>.%
\end{warn}\<close>
subsubsection \<open>Semigroups\<close>
--- a/src/Doc/Tutorial/Types/Records.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Tutorial/Types/Records.thy Sun Jan 15 18:30:18 2023 +0100
@@ -33,7 +33,7 @@
text \<open>
Record types are not primitive in Isabelle and have a delicate
- internal representation @{cite "NaraschewskiW-TPHOLs98"}, based on
+ internal representation \<^cite>\<open>"NaraschewskiW-TPHOLs98"\<close>, based on
nested copies of the primitive product type. A \commdx{record}
declaration introduces a new record type scheme by specifying its
fields, which are packaged internally to hold up the perception of
--- a/src/Doc/Tutorial/Types/Typedefs.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Tutorial/Types/Typedefs.thy Sun Jan 15 18:30:18 2023 +0100
@@ -213,7 +213,7 @@
example to demonstrate \isacommand{typedef} because its simplicity makes the
key concepts particularly easy to grasp. If you would like to see a
non-trivial example that cannot be defined more directly, we recommend the
-definition of \emph{finite multisets} in the Library~@{cite "HOL-Library"}.
+definition of \emph{finite multisets} in the Library~\<^cite>\<open>"HOL-Library"\<close>.
Let us conclude by summarizing the above procedure for defining a new type.
Given some abstract axiomatic description $P$ of a type $ty$ in terms of a
--- a/src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy Sun Jan 15 18:30:18 2023 +0100
@@ -28,8 +28,8 @@
instantiating type-classes, adding relationships between
locales (@{command sublocale}) and type-classes
(@{command subclass}). Handy introductions are the
- respective tutorials @{cite "isabelle-locale"}
- @{cite "isabelle-classes"}.
+ respective tutorials \<^cite>\<open>"isabelle-locale"\<close>
+ \<^cite>\<open>"isabelle-classes"\<close>.
\<close>
subsection \<open>Strengths and restrictions of type classes\<close>
@@ -48,7 +48,7 @@
to the numerical type on the right hand side.
How to accomplish this given the quite restrictive type system
- of {Isabelle/HOL}? Paulson @{cite "paulson-numerical"} explains
+ of {Isabelle/HOL}? Paulson \<^cite>\<open>"paulson-numerical"\<close> explains
that each numerical type has some characteristic properties
which define an characteristic algebraic structure; \<open>\<sqsubset>\<close>
then corresponds to specialization of the corresponding
@@ -122,7 +122,7 @@
optionally showing the logical content for each class also.
Optional parameters restrict the graph to a particular segment
which is useful to get a graspable view. See
- the Isar reference manual @{cite "isabelle-isar-ref"} for details.
+ the Isar reference manual \<^cite>\<open>"isabelle-isar-ref"\<close> for details.
\<close>
@@ -144,7 +144,7 @@
\<^item> @{command class} \<^class>\<open>one\<close> with @{term [source] "1::'a::one"}
\noindent Before the introduction of the @{command class} statement in
- Isabelle @{cite "Haftmann-Wenzel:2006:classes"} it was impossible
+ Isabelle \<^cite>\<open>"Haftmann-Wenzel:2006:classes"\<close> it was impossible
to define operations with associated axioms in the same class,
hence there were always pairs of syntactic and logical type
classes. This restriction is lifted nowadays, but there are
--- a/src/HOL/Algebra/Group.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Algebra/Group.thy Sun Jan 15 18:30:18 2023 +0100
@@ -14,7 +14,7 @@
subsection \<open>Definitions\<close>
text \<open>
- Definitions follow @{cite "Jacobson:1985"}.
+ Definitions follow \<^cite>\<open>"Jacobson:1985"\<close>.
\<close>
record 'a monoid = "'a partial_object" +
--- a/src/HOL/Algebra/Multiplicative_Group.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Algebra/Multiplicative_Group.thy Sun Jan 15 18:30:18 2023 +0100
@@ -904,7 +904,7 @@
text \<open>
In this section we show that the multiplicative group of a finite field
is generated by a single element, i.e. it is cyclic. The proof is inspired
- by the first proof given in the survey~@{cite "conrad-cyclicity"}.
+ by the first proof given in the survey~\<^cite>\<open>"conrad-cyclicity"\<close>.
\<close>
context field begin
--- a/src/HOL/Algebra/Sylow.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Algebra/Sylow.thy Sun Jan 15 18:30:18 2023 +0100
@@ -6,7 +6,7 @@
imports Coset Exponent
begin
-text \<open>See also @{cite "Kammueller-Paulson:1999"}.\<close>
+text \<open>See also \<^cite>\<open>"Kammueller-Paulson:1999"\<close>.\<close>
text \<open>The combinatorial argument is in theory \<open>Exponent\<close>.\<close>
--- a/src/HOL/Algebra/UnivPoly.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy Sun Jan 15 18:30:18 2023 +0100
@@ -18,7 +18,7 @@
carrier set is a set of bounded functions from Nat to the
coefficient domain. Bounded means that these functions return zero
above a certain bound (the degree). There is a chapter on the
- formalisation of polynomials in the PhD thesis @{cite "Ballarin:1999"},
+ formalisation of polynomials in the PhD thesis \<^cite>\<open>"Ballarin:1999"\<close>,
which was implemented with axiomatic type classes. This was later
ported to Locales.
\<close>
--- a/src/HOL/Analysis/Continuous_Extension.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Analysis/Continuous_Extension.thy Sun Jan 15 18:30:18 2023 +0100
@@ -296,7 +296,7 @@
subsection\<open>Dugundji's Extension Theorem and Tietze Variants\<close>
-text \<open>See \cite{dugundji}.\<close>
+text \<open>See \<^cite>\<open>"dugundji"\<close>.\<close>
lemma convex_supp_sum:
assumes "convex S" and 1: "supp_sum u I = 1"
--- a/src/HOL/Analysis/Infinite_Sum.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Analysis/Infinite_Sum.thy Sun Jan 15 18:30:18 2023 +0100
@@ -17,7 +17,7 @@
Our definition is quite standard: $s:=\sum_{x\in A} f(x)$ is the limit of finite sums $s_F:=\sum_{x\in F} f(x)$ for increasing $F$.
That is, $s$ is the limit of the net $s_F$ where $F$ are finite subsets of $A$ ordered by inclusion.
We believe that this is the standard definition for such sums.
-See, e.g., Definition 4.11 in \cite{conway2013course}.
+See, e.g., Definition 4.11 in \<^cite>\<open>"conway2013course"\<close>.
This definition is quite general: it is well-defined whenever $f$ takes values in some
commutative monoid endowed with a Hausdorff topology.
(Examples are reals, complex numbers, normed vector spaces, and more.)\<close>
--- a/src/HOL/Analysis/Metric_Arith.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Analysis/Metric_Arith.thy Sun Jan 15 18:30:18 2023 +0100
@@ -12,7 +12,7 @@
text\<^marker>\<open>tag unimportant\<close> \<open>
A port of the decision procedure ``Formalization of metric spaces in HOL Light''
-@{cite "DBLP:journals/jar/Maggesi18"} for the type class @{class metric_space},
+\<^cite>\<open>"DBLP:journals/jar/Maggesi18"\<close> for the type class @{class metric_space},
with the \<open>Argo\<close> solver as backend.
\<close>
--- a/src/HOL/Data_Structures/Braun_Tree.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Data_Structures/Braun_Tree.thy Sun Jan 15 18:30:18 2023 +0100
@@ -6,8 +6,8 @@
imports "HOL-Library.Tree_Real"
begin
-text \<open>Braun Trees were studied by Braun and Rem~\cite{BraunRem}
-and later Hoogerwoord~\cite{Hoogerwoord}.\<close>
+text \<open>Braun Trees were studied by Braun and Rem~\<^cite>\<open>"BraunRem"\<close>
+and later Hoogerwoord~\<^cite>\<open>"Hoogerwoord"\<close>.\<close>
fun braun :: "'a tree \<Rightarrow> bool" where
"braun Leaf = True" |
--- a/src/HOL/Examples/Cantor.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Examples/Cantor.thy Sun Jan 15 18:30:18 2023 +0100
@@ -81,7 +81,7 @@
text \<open>
The following treatment of Cantor's Theorem follows the classic example from
the early 1990s, e.g.\ see the file \<^verbatim>\<open>92/HOL/ex/set.ML\<close> in
- Isabelle92 or @{cite \<open>\S18.7\<close> "paulson-isa-book"}. The old tactic scripts
+ Isabelle92 or \<^cite>\<open>\<open>\S18.7\<close> in "paulson-isa-book"\<close>. The old tactic scripts
synthesize key information of the proof by refinement of schematic goal
states. In contrast, the Isar proof needs to say explicitly what is proven.
--- a/src/HOL/Examples/Knaster_Tarski.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Examples/Knaster_Tarski.thy Sun Jan 15 18:30:18 2023 +0100
@@ -16,7 +16,7 @@
subsection \<open>Prose version\<close>
text \<open>
- According to the textbook @{cite \<open>pages 93--94\<close> "davey-priestley"}, the
+ According to the textbook \<^cite>\<open>\<open>pages 93--94\<close> in "davey-priestley"\<close>, the
Knaster-Tarski fixpoint theorem is as follows.\<^footnote>\<open>We have dualized the
argument, and tuned the notation a little bit.\<close>
--- a/src/HOL/HOLCF/IMP/HoareEx.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/HOLCF/IMP/HoareEx.thy Sun Jan 15 18:30:18 2023 +0100
@@ -9,7 +9,7 @@
text \<open>
An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch
- @{cite MuellerNvOS99}. It demonstrates fixpoint reasoning by showing
+ \<^cite>\<open>MuellerNvOS99\<close>. It demonstrates fixpoint reasoning by showing
the correctness of the Hoare rule for while-loops.
\<close>
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy Sun Jan 15 18:30:18 2023 +0100
@@ -10,7 +10,7 @@
text \<open>
We present the proof of two different versions of the Hahn-Banach Theorem,
- closely following @{cite \<open>\S36\<close> "Heuser:1986"}.
+ closely following \<^cite>\<open>\<open>\S36\<close> in "Heuser:1986"\<close>.
\<close>
--- a/src/HOL/Imperative_HOL/Overview.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Imperative_HOL/Overview.thy Sun Jan 15 18:30:18 2023 +0100
@@ -20,8 +20,8 @@
text \<open>
\<open>Imperative HOL\<close> is a lightweight framework for reasoning
about imperative data structures in \<open>Isabelle/HOL\<close>
- @{cite "Nipkow-et-al:2002:tutorial"}. Its basic ideas are described in
- @{cite "Bulwahn-et-al:2008:imp_HOL"}. However their concrete
+ \<^cite>\<open>"Nipkow-et-al:2002:tutorial"\<close>. Its basic ideas are described in
+ \<^cite>\<open>"Bulwahn-et-al:2008:imp_HOL"\<close>. However their concrete
realisation has changed since, due to both extensions and
refinements. Therefore this overview wants to present the framework
\qt{as it is} by now. It focusses on the user-view, less on matters
--- a/src/HOL/Induct/Comb.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Induct/Comb.thy Sun Jan 15 18:30:18 2023 +0100
@@ -11,7 +11,7 @@
text \<open>
Combinator terms do not have free variables.
- Example taken from @{cite camilleri92}.
+ Example taken from \<^cite>\<open>camilleri92\<close>.
\<close>
subsection \<open>Definitions\<close>
--- a/src/HOL/Isar_Examples/Basic_Logic.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Isar_Examples/Basic_Logic.thy Sun Jan 15 18:30:18 2023 +0100
@@ -250,8 +250,7 @@
subsection \<open>A few examples from ``Introduction to Isabelle''\<close>
text \<open>
- We rephrase some of the basic reasoning examples of @{cite
- "isabelle-intro"}, using HOL rather than FOL.
+ We rephrase some of the basic reasoning examples of \<^cite>\<open>"isabelle-intro"\<close>, using HOL rather than FOL.
\<close>
--- a/src/HOL/Isar_Examples/Fibonacci.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Isar_Examples/Fibonacci.thy Sun Jan 15 18:30:18 2023 +0100
@@ -19,7 +19,7 @@
begin
text_raw \<open>\<^footnote>\<open>Isar version by Gertrud Bauer. Original tactic script by Larry
- Paulson. A few proofs of laws taken from @{cite "Concrete-Math"}.\<close>\<close>
+ Paulson. A few proofs of laws taken from \<^cite>\<open>"Concrete-Math"\<close>.\<close>\<close>
subsection \<open>Fibonacci numbers\<close>
@@ -42,11 +42,11 @@
subsection \<open>Fib and gcd commute\<close>
-text \<open>A few laws taken from @{cite "Concrete-Math"}.\<close>
+text \<open>A few laws taken from \<^cite>\<open>"Concrete-Math"\<close>.\<close>
lemma fib_add: "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
(is "?P n")
- \<comment> \<open>see @{cite \<open>page 280\<close> "Concrete-Math"}\<close>
+ \<comment> \<open>see \<^cite>\<open>\<open>page 280\<close> in "Concrete-Math"\<close>\<close>
proof (induct n rule: fib_induct)
show "?P 0" by simp
show "?P 1" by simp
--- a/src/HOL/Isar_Examples/Hoare.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy Sun Jan 15 18:30:18 2023 +0100
@@ -15,8 +15,8 @@
text \<open>
The following abstract syntax and semantics of Hoare Logic over \<^verbatim>\<open>WHILE\<close>
programs closely follows the existing tradition in Isabelle/HOL of
- formalizing the presentation given in @{cite \<open>\S6\<close> "Winskel:1993"}. See also
- \<^dir>\<open>~~/src/HOL/Hoare\<close> and @{cite "Nipkow:1998:Winskel"}.
+ formalizing the presentation given in \<^cite>\<open>\<open>\S6\<close> in "Winskel:1993"\<close>. See also
+ \<^dir>\<open>~~/src/HOL/Hoare\<close> and \<^cite>\<open>"Nipkow:1998:Winskel"\<close>.
\<close>
type_synonym 'a bexp = "'a set"
@@ -60,7 +60,7 @@
text \<open>
From the semantics defined above, we derive the standard set of primitive
- Hoare rules; e.g.\ see @{cite \<open>\S6\<close> "Winskel:1993"}. Usually, variant forms
+ Hoare rules; e.g.\ see \<^cite>\<open>\<open>\S6\<close> in "Winskel:1993"\<close>. Usually, variant forms
of these rules are applied in actual proof, see also \S\ref{sec:hoare-isar}
and \S\ref{sec:hoare-vcg}.
@@ -304,8 +304,7 @@
text \<open>
Note that above formulation of assignment corresponds to our preferred way
- to model state spaces, using (extensible) record types in HOL @{cite
- "Naraschewski-Wenzel:1998:HOOL"}. For any record field \<open>x\<close>, Isabelle/HOL
+ to model state spaces, using (extensible) record types in HOL \<^cite>\<open>"Naraschewski-Wenzel:1998:HOOL"\<close>. For any record field \<open>x\<close>, Isabelle/HOL
provides a functions \<open>x\<close> (selector) and \<open>x_update\<close> (update). Above, there is
only a place-holder appearing for the latter kind of function: due to
concrete syntax \<open>\<acute>x := \<acute>a\<close> also contains \<open>x_update\<close>.\<^footnote>\<open>Note that due to the
--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Sun Jan 15 18:30:18 2023 +0100
@@ -10,8 +10,7 @@
begin
text \<open>
- The Mutilated Checker Board Problem, formalized inductively. See @{cite
- "paulson-mutilated-board"} for the original tactic script version.
+ The Mutilated Checker Board Problem, formalized inductively. See \<^cite>\<open>"paulson-mutilated-board"\<close> for the original tactic script version.
\<close>
subsection \<open>Tilings\<close>
--- a/src/HOL/Lattice/CompleteLattice.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Lattice/CompleteLattice.thy Sun Jan 15 18:30:18 2023 +0100
@@ -106,7 +106,7 @@
text \<open>
The Knaster-Tarski Theorem (in its simplest formulation) states that
any monotone function on a complete lattice has a least fixed-point
- (see @{cite \<open>pages 93--94\<close> "Davey-Priestley:1990"} for example). This
+ (see \<^cite>\<open>\<open>pages 93--94\<close> in "Davey-Priestley:1990"\<close> for example). This
is a consequence of the basic boundary properties of the complete
lattice operations.
\<close>
--- a/src/HOL/Library/BigO.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Library/BigO.thy Sun Jan 15 18:30:18 2023 +0100
@@ -14,8 +14,7 @@
text \<open>
This library is designed to support asymptotic ``big O'' calculations,
i.e.~reasoning with expressions of the form \<open>f = O(g)\<close> and \<open>f = g + O(h)\<close>.
- An earlier version of this library is described in detail in @{cite
- "Avigad-Donnelly"}.
+ An earlier version of this library is described in detail in \<^cite>\<open>"Avigad-Donnelly"\<close>.
The main changes in this version are as follows:
--- a/src/HOL/Library/Code_Lazy.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Library/Code_Lazy.thy Sun Jan 15 18:30:18 2023 +0100
@@ -15,7 +15,7 @@
begin
text \<open>
- This theory and the CodeLazy tool described in @{cite "LochbihlerStoop2018"}.
+ This theory and the CodeLazy tool described in \<^cite>\<open>"LochbihlerStoop2018"\<close>.
It hooks into Isabelle's code generator such that the generated code evaluates a user-specified
set of type constructors lazily, even in target languages with eager evaluation.
--- a/src/HOL/Library/Poly_Mapping.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Library/Poly_Mapping.thy Sun Jan 15 18:30:18 2023 +0100
@@ -295,7 +295,7 @@
to coefficients. Lets call this the \emph{ultimate interpretation}.
\item A further more specialised type isomorphic to @{typ "nat \<Rightarrow>\<^sub>0 'a"}
is apt to direct implementation using code generation
- \cite{Haftmann-Nipkow:2010:code}.
+ \<^cite>\<open>"Haftmann-Nipkow:2010:code"\<close>.
\end{enumerate}
Note that despite the names \emph{mapping} and \emph{lookup} suggest something
implementation-near, it is best to keep @{typ "'a \<Rightarrow>\<^sub>0 'b"} as an abstract
--- a/src/HOL/Library/Ramsey.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Library/Ramsey.thy Sun Jan 15 18:30:18 2023 +0100
@@ -916,7 +916,7 @@
text \<open>
An application of Ramsey's theorem to program termination. See
- @{cite "Podelski-Rybalchenko"}.
+ \<^cite>\<open>"Podelski-Rybalchenko"\<close>.
\<close>
definition disj_wf :: "('a \<times> 'a) set \<Rightarrow> bool"
--- a/src/HOL/Proofs/Extraction/Euclid.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Proofs/Extraction/Euclid.thy Sun Jan 15 18:30:18 2023 +0100
@@ -16,7 +16,7 @@
text \<open>
A constructive version of the proof of Euclid's theorem by
- Markus Wenzel and Freek Wiedijk @{cite "Wenzel-Wiedijk-JAR2002"}.
+ Markus Wenzel and Freek Wiedijk \<^cite>\<open>"Wenzel-Wiedijk-JAR2002"\<close>.
\<close>
lemma factor_greater_one1: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < m"
--- a/src/HOL/Proofs/Extraction/Higman.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Proofs/Extraction/Higman.thy Sun Jan 15 18:30:18 2023 +0100
@@ -11,7 +11,7 @@
text \<open>
Formalization by Stefan Berghofer and Monika Seisenberger,
- based on Coquand and Fridlender @{cite Coquand93}.
+ based on Coquand and Fridlender \<^cite>\<open>Coquand93\<close>.
\<close>
datatype letter = A | B
--- a/src/HOL/Proofs/Extraction/Pigeonhole.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy Sun Jan 15 18:30:18 2023 +0100
@@ -12,7 +12,7 @@
We formalize two proofs of the pigeonhole principle, which lead
to extracted programs of quite different complexity. The original
formalization of these proofs in {\sc Nuprl} is due to
- Aleksey Nogin @{cite "Nogin-ENTCS-2000"}.
+ Aleksey Nogin \<^cite>\<open>"Nogin-ENTCS-2000"\<close>.
This proof yields a polynomial program.
\<close>
--- a/src/HOL/Proofs/Extraction/Warshall.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Proofs/Extraction/Warshall.thy Sun Jan 15 18:30:18 2023 +0100
@@ -10,7 +10,7 @@
text \<open>
Derivation of Warshall's algorithm using program extraction,
- based on Berger, Schwichtenberg and Seisenberger @{cite "Berger-JAR-2001"}.
+ based on Berger, Schwichtenberg and Seisenberger \<^cite>\<open>"Berger-JAR-2001"\<close>.
\<close>
datatype b = T | F
--- a/src/HOL/Proofs/Lambda/Eta.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Proofs/Lambda/Eta.thy Sun Jan 15 18:30:18 2023 +0100
@@ -230,7 +230,7 @@
text \<open>
Based on a paper proof due to Andreas Abel.
- Unlike the proof by Masako Takahashi @{cite "Takahashi-IandC"}, it does not
+ Unlike the proof by Masako Takahashi \<^cite>\<open>"Takahashi-IandC"\<close>, it does not
use parallel eta reduction, which only seems to complicate matters unnecessarily.
\<close>
--- a/src/HOL/Proofs/Lambda/Standardization.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Proofs/Lambda/Standardization.thy Sun Jan 15 18:30:18 2023 +0100
@@ -10,8 +10,8 @@
begin
text \<open>
-Based on lecture notes by Ralph Matthes @{cite "Matthes-ESSLLI2000"},
-original proof idea due to Ralph Loader @{cite Loader1998}.
+Based on lecture notes by Ralph Matthes \<^cite>\<open>"Matthes-ESSLLI2000"\<close>,
+original proof idea due to Ralph Loader \<^cite>\<open>Loader1998\<close>.
\<close>
--- a/src/HOL/Proofs/Lambda/StrongNorm.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Proofs/Lambda/StrongNorm.thy Sun Jan 15 18:30:18 2023 +0100
@@ -9,7 +9,7 @@
text \<open>
Formalization by Stefan Berghofer. Partly based on a paper proof by
-Felix Joachimski and Ralph Matthes @{cite "Matthes-Joachimski-AML"}.
+Felix Joachimski and Ralph Matthes \<^cite>\<open>"Matthes-Joachimski-AML"\<close>.
\<close>
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy Sun Jan 15 18:30:18 2023 +0100
@@ -11,7 +11,7 @@
text \<open>
Formalization by Stefan Berghofer. Partly based on a paper proof by
-Felix Joachimski and Ralph Matthes @{cite "Matthes-Joachimski-AML"}.
+Felix Joachimski and Ralph Matthes \<^cite>\<open>"Matthes-Joachimski-AML"\<close>.
\<close>
--- a/src/HOL/SPARK/Manual/Example_Verification.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/SPARK/Manual/Example_Verification.thy Sun Jan 15 18:30:18 2023 +0100
@@ -23,7 +23,7 @@
We will now explain the usage of the \SPARK{} verification environment by proving
the correctness of an example program. As an example, we use a program for computing
the \emph{greatest common divisor} of two natural numbers shown in \figref{fig:gcd-prog},
-which has been taken from the book about \SPARK{} by Barnes @{cite \<open>\S 11.6\<close> Barnes}.
+which has been taken from the book about \SPARK{} by Barnes \<^cite>\<open>\<open>\S 11.6\<close> in Barnes\<close>.
\<close>
section \<open>Importing \SPARK{} VCs into Isabelle\<close>
@@ -228,7 +228,7 @@
are trivially proved to be non-negative. Since we are working with non-negative
numbers, we can also just use \SPARK{}'s \textbf{mod} operator instead of
\textbf{rem}, which spares us an application of theorems \<open>minus_div_mult_eq_mod [symmetric]\<close>
-and \<open>sdiv_pos_pos\<close>. Finally, as noted by Barnes @{cite \<open>\S 11.5\<close> Barnes},
+and \<open>sdiv_pos_pos\<close>. Finally, as noted by Barnes \<^cite>\<open>\<open>\S 11.5\<close> in Barnes\<close>,
we can simplify matters by placing the \textbf{assert} statement between
\textbf{while} and \textbf{loop} rather than directly after the \textbf{loop}.
In the former case, the loop invariant has to be proved only once, whereas in
--- a/src/HOL/SPARK/Manual/VC_Principles.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/SPARK/Manual/VC_Principles.thy Sun Jan 15 18:30:18 2023 +0100
@@ -76,7 +76,7 @@
\caption{Control flow graph for procedure \texttt{Proc2}}
\label{fig:proc2-graph}
\end{figure}
-As explained by Barnes @{cite \<open>\S 11.5\<close> Barnes}, the \SPARK{} Examiner unfolds the loop
+As explained by Barnes \<^cite>\<open>\<open>\S 11.5\<close> in Barnes\<close>, the \SPARK{} Examiner unfolds the loop
\begin{lstlisting}
for I in T range L .. U loop
--# assert P (I);
--- a/src/HOL/Unix/Unix.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Unix/Unix.thy Sun Jan 15 18:30:18 2023 +0100
@@ -67,7 +67,7 @@
simplification as we just do not intend to discuss a model of multiple
groups and group membership, but pretend that everyone is member of a single
global group.\<^footnote>\<open>A general HOL model of user group structures and related
- issues is given in @{cite "Naraschewski:2001"}.\<close>
+ issues is given in \<^cite>\<open>"Naraschewski:2001"\<close>.\<close>
\<close>
datatype perm =
@@ -104,7 +104,7 @@
text \<open>
In order to model the general tree structure of a Unix file-system we use
the arbitrarily branching datatype \<^typ>\<open>('a, 'b, 'c) env\<close> from the
- standard library of Isabelle/HOL @{cite "Bauer-et-al:2002:HOL-Library"}.
+ standard library of Isabelle/HOL \<^cite>\<open>"Bauer-et-al:2002:HOL-Library"\<close>.
This type provides constructors \<^term>\<open>Val\<close> and \<^term>\<open>Env\<close> as follows:
\<^medskip>
@@ -142,15 +142,14 @@
@{thm [display, indent = 2, eta_contract = false] lookup_eq [no_vars]}
@{thm [display, indent = 2, eta_contract = false] update_eq [no_vars]}
- Several further properties of these operations are proven in @{cite
- "Bauer-et-al:2002:HOL-Library"}. These will be routinely used later on
+ Several further properties of these operations are proven in \<^cite>\<open>"Bauer-et-al:2002:HOL-Library"\<close>. These will be routinely used later on
without further notice.
\<^bigskip>
Apparently, the elements of type \<^typ>\<open>file\<close> contain an \<^typ>\<open>att\<close>
component in either case. We now define a few auxiliary operations to
manipulate this field uniformly, following the conventions for record types
- in Isabelle/HOL @{cite "Nipkow-et-al:2000:HOL"}.
+ in Isabelle/HOL \<^cite>\<open>"Nipkow-et-al:2000:HOL"\<close>.
\<close>
definition
@@ -208,8 +207,7 @@
access was granted according to the permissions recorded within the
file-system.
- Note that by the rules of Unix file-system security (e.g.\ @{cite
- "Tanenbaum:1992"}) both the super-user and owner may always access a file
+ Note that by the rules of Unix file-system security (e.g.\ \<^cite>\<open>"Tanenbaum:1992"\<close>) both the super-user and owner may always access a file
unconditionally (in our simplified model).
\<close>
@@ -264,8 +262,7 @@
subsection \<open>Unix system calls \label{sec:unix-syscall}\<close>
text \<open>
- According to established operating system design (cf.\ @{cite
- "Tanenbaum:1992"}) user space processes may only initiate system operations
+ According to established operating system design (cf.\ \<^cite>\<open>"Tanenbaum:1992"\<close>) user space processes may only initiate system operations
by a fixed set of \<^emph>\<open>system-calls\<close>. This enables the kernel to enforce
certain security policies in the first place.\<^footnote>\<open>Incidently, this is the very
same principle employed by any ``LCF-style'' theorem proving system
@@ -388,7 +385,7 @@
If in doubt, one may consider to compare our definition with the informal
specifications given the corresponding Unix man pages, or even peek at an
- actual implementation such as @{cite "Torvalds-et-al:Linux"}. Another common
+ actual implementation such as \<^cite>\<open>"Torvalds-et-al:Linux"\<close>. Another common
way to gain confidence into the formal model is to run simple simulations
(see \secref{sec:unix-examples}), and check the results with that of
experiments performed on a real Unix system.
--- a/src/HOL/ex/CTL.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/ex/CTL.thy Sun Jan 15 18:30:18 2023 +0100
@@ -9,8 +9,7 @@
begin
text \<open>
- We formalize basic concepts of Computational Tree Logic (CTL) @{cite
- "McMillan-PhDThesis" and "McMillan-LectureNotes"} within the simply-typed
+ We formalize basic concepts of Computational Tree Logic (CTL) \<^cite>\<open>"McMillan-PhDThesis" and "McMillan-LectureNotes"\<close> within the simply-typed
set theory of HOL.
By using the common technique of ``shallow embedding'', a CTL formula is
@@ -51,7 +50,7 @@
holds in a state \<open>s\<close>, iff there is a path, starting from \<open>s\<close>, such that for
all states \<open>s'\<close> on the path, \<open>p\<close> holds in \<open>s'\<close>. It is easy to see that \<open>\<^bold>E\<^bold>F
p\<close> and \<open>\<^bold>E\<^bold>G p\<close> may be expressed using least and greatest fixed points
- @{cite "McMillan-PhDThesis"}.
+ \<^cite>\<open>"McMillan-PhDThesis"\<close>.
\<close>
definition EX ("\<^bold>E\<^bold>X _" [80] 90)
--- a/src/Pure/Examples/Higher_Order_Logic.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Pure/Examples/Higher_Order_Logic.thy Sun Jan 15 18:30:18 2023 +0100
@@ -10,8 +10,7 @@
text \<open>
The following theory development illustrates the foundations of Higher-Order
- Logic. The ``HOL'' logic that is given here resembles @{cite
- "Gordon:1985:HOL"} and its predecessor @{cite "church40"}, but the order of
+ Logic. The ``HOL'' logic that is given here resembles \<^cite>\<open>"Gordon:1985:HOL"\<close> and its predecessor \<^cite>\<open>"church40"\<close>, but the order of
axiomatizations and defined connectives has be adapted to modern
presentations of \<open>\<lambda>\<close>-calculus and Constructive Type Theory. Thus it fits
nicely to the underlying Natural Deduction framework of Isabelle/Pure and
--- a/src/ZF/Induct/Acc.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/ZF/Induct/Acc.thy Sun Jan 15 18:30:18 2023 +0100
@@ -8,7 +8,7 @@
theory Acc imports ZF begin
text \<open>
- Inductive definition of \<open>acc(r)\<close>; see @{cite "paulin-tlca"}.
+ Inductive definition of \<open>acc(r)\<close>; see \<^cite>\<open>"paulin-tlca"\<close>.
\<close>
consts
--- a/src/ZF/Induct/Comb.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/ZF/Induct/Comb.thy Sun Jan 15 18:30:18 2023 +0100
@@ -12,7 +12,7 @@
text \<open>
Curiously, combinators do not include free variables.
- Example taken from @{cite camilleri92}.
+ Example taken from \<^cite>\<open>camilleri92\<close>.
\<close>
--- a/src/ZF/Induct/ListN.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/ZF/Induct/ListN.thy Sun Jan 15 18:30:18 2023 +0100
@@ -9,7 +9,7 @@
text \<open>
Inductive definition of lists of \<open>n\<close> elements; see
- @{cite "paulin-tlca"}.
+ \<^cite>\<open>"paulin-tlca"\<close>.
\<close>
consts listn :: "i\<Rightarrow>i"
--- a/src/ZF/Induct/Primrec.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/ZF/Induct/Primrec.thy Sun Jan 15 18:30:18 2023 +0100
@@ -8,9 +8,9 @@
theory Primrec imports ZF begin
text \<open>
- Proof adopted from @{cite szasz93}.
+ Proof adopted from \<^cite>\<open>szasz93\<close>.
- See also @{cite \<open>page 250, exercise 11\<close> mendelson}.
+ See also \<^cite>\<open>\<open>page 250, exercise 11\<close> in mendelson\<close>.
\<close>