more antiquotations;
authorwenzelm
Tue Oct 07 22:35:11 2014 +0200 (2014-10-07)
changeset 586207435b6a3f72e
parent 58619 4b41df5fef81
child 58621 7a2c567061b3
more antiquotations;
src/Doc/Classes/Classes.thy
src/Doc/Codegen/Evaluation.thy
src/Doc/Codegen/Further.thy
src/Doc/Codegen/Inductive_Predicate.thy
src/Doc/Codegen/Introduction.thy
src/Doc/Codegen/Refinement.thy
src/Doc/Datatypes/Datatypes.thy
src/Doc/Functions/Functions.thy
src/Doc/Locales/Examples.thy
src/Doc/Locales/Examples3.thy
src/Doc/Logics_ZF/ZF_Isar.thy
src/Doc/Prog_Prove/Logic.thy
src/Doc/Prog_Prove/Types_and_funs.thy
src/Doc/Sugar/Sugar.thy
src/Doc/Tutorial/Advanced/WFrec.thy
src/Doc/Tutorial/Advanced/simp2.thy
src/Doc/Tutorial/CTL/Base.thy
src/Doc/Tutorial/CTL/CTL.thy
src/Doc/Tutorial/CTL/PDL.thy
src/Doc/Tutorial/Datatype/Nested.thy
src/Doc/Tutorial/Documents/Documents.thy
src/Doc/Tutorial/Fun/fun0.thy
src/Doc/Tutorial/Inductive/AB.thy
src/Doc/Tutorial/Protocol/NS_Public.thy
src/Doc/Tutorial/Types/Axioms.thy
src/Doc/Tutorial/Types/Records.thy
src/Doc/Tutorial/Types/Typedefs.thy
     1.1 --- a/src/Doc/Classes/Classes.thy	Tue Oct 07 21:44:41 2014 +0200
     1.2 +++ b/src/Doc/Classes/Classes.thy	Tue Oct 07 22:35:11 2014 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  section {* Introduction *}
     1.5  
     1.6  text {*
     1.7 -  Type classes were introduced by Wadler and Blott \cite{wadler89how}
     1.8 +  Type classes were introduced by Wadler and Blott @{cite wadler89how}
     1.9    into the Haskell language to allow for a reasonable implementation
    1.10    of overloading\footnote{throughout this tutorial, we are referring
    1.11    to classical Haskell 1.0 type classes, not considering later
    1.12 @@ -43,7 +43,7 @@
    1.13  
    1.14    Indeed, type classes not only allow for simple overloading but form
    1.15    a generic calculus, an instance of order-sorted algebra
    1.16 -  \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
    1.17 +  @{cite "nipkow-sorts93" and "Nipkow-Prehofer:1993" and "Wenzel:1997:TPHOL"}.
    1.18  
    1.19    From a software engineering point of view, type classes roughly
    1.20    correspond to interfaces in object-oriented languages like Java; so,
    1.21 @@ -67,7 +67,7 @@
    1.22  
    1.23    \noindent From a theoretical point of view, type classes are
    1.24    lightweight modules; Haskell type classes may be emulated by SML
    1.25 -  functors \cite{classes_modules}.  Isabelle/Isar offers a discipline
    1.26 +  functors @{cite classes_modules}.  Isabelle/Isar offers a discipline
    1.27    of type classes which brings all those aspects together:
    1.28  
    1.29    \begin{enumerate}
    1.30 @@ -77,17 +77,17 @@
    1.31         type
    1.32      \item in connection with a ``less ad-hoc'' approach to overloading,
    1.33      \item with a direct link to the Isabelle module system:
    1.34 -      locales \cite{kammueller-locales}.
    1.35 +      locales @{cite "kammueller-locales"}.
    1.36    \end{enumerate}
    1.37  
    1.38    \noindent Isar type classes also directly support code generation in
    1.39    a Haskell like fashion. Internally, they are mapped to more
    1.40 -  primitive Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
    1.41 +  primitive Isabelle concepts @{cite "Haftmann-Wenzel:2006:classes"}.
    1.42  
    1.43    This tutorial demonstrates common elements of structured
    1.44    specifications and abstract reasoning with type classes by the
    1.45    algebraic hierarchy of semigroups, monoids and groups.  Our
    1.46 -  background theory is that of Isabelle/HOL \cite{isa-tutorial}, for
    1.47 +  background theory is that of Isabelle/HOL @{cite "isa-tutorial"}, for
    1.48    which some familiarity is assumed.
    1.49  *}
    1.50  
    1.51 @@ -423,7 +423,7 @@
    1.52    \noindent As you can see from this example, for local definitions
    1.53    you may use any specification tool which works together with
    1.54    locales, such as Krauss's recursive function package
    1.55 -  \cite{krauss2006}.
    1.56 +  @{cite krauss2006}.
    1.57  *}
    1.58  
    1.59  
    1.60 @@ -583,7 +583,7 @@
    1.61    overloading, it is obvious that overloading stemming from @{command
    1.62    class} statements and @{command instantiation} targets naturally
    1.63    maps to Haskell type classes.  The code generator framework
    1.64 -  \cite{isabelle-codegen} takes this into account.  If the target
    1.65 +  @{cite "isabelle-codegen"} takes this into account.  If the target
    1.66    language (e.g.~SML) lacks type classes, then they are implemented by
    1.67    an explicit dictionary construction.  As example, let's go back to
    1.68    the power function:
     2.1 --- a/src/Doc/Codegen/Evaluation.thy	Tue Oct 07 21:44:41 2014 +0200
     2.2 +++ b/src/Doc/Codegen/Evaluation.thy	Tue Oct 07 22:35:11 2014 +0200
     2.3 @@ -53,7 +53,7 @@
     2.4  subsubsection {* Normalization by evaluation (@{text nbe}) *}
     2.5  
     2.6  text {*
     2.7 -  Normalization by evaluation \cite{Aehlig-Haftmann-Nipkow:2008:nbe}
     2.8 +  Normalization by evaluation @{cite "Aehlig-Haftmann-Nipkow:2008:nbe"}
     2.9    provides a comparably fast partially symbolic evaluation which
    2.10    permits also normalization of functions and uninterpreted symbols;
    2.11    the stack of code to be trusted is considerable.
     3.1 --- a/src/Doc/Codegen/Further.thy	Tue Oct 07 21:44:41 2014 +0200
     3.2 +++ b/src/Doc/Codegen/Further.thy	Tue Oct 07 22:35:11 2014 +0200
     3.3 @@ -183,7 +183,7 @@
     3.4    can be generated.  But this not the case: internally, the term
     3.5    @{text "fun_power.powers"} is an abbreviation for the foundational
     3.6    term @{term [source] "power.powers (\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"}
     3.7 -  (see \cite{isabelle-locale} for the details behind).
     3.8 +  (see @{cite "isabelle-locale"} for the details behind).
     3.9  
    3.10    Fortunately, with minor effort the desired behaviour can be
    3.11    achieved.  First, a dedicated definition of the constant on which
    3.12 @@ -233,7 +233,7 @@
    3.13    If you consider imperative data structures as inevitable for a
    3.14    specific application, you should consider \emph{Imperative
    3.15    Functional Programming with Isabelle/HOL}
    3.16 -  \cite{bulwahn-et-al:2008:imperative}; the framework described there
    3.17 +  @{cite "bulwahn-et-al:2008:imperative"}; the framework described there
    3.18    is available in session @{text Imperative_HOL}, together with a
    3.19    short primer document.
    3.20  *}
     4.1 --- a/src/Doc/Codegen/Inductive_Predicate.thy	Tue Oct 07 21:44:41 2014 +0200
     4.2 +++ b/src/Doc/Codegen/Inductive_Predicate.thy	Tue Oct 07 22:35:11 2014 +0200
     4.3 @@ -23,7 +23,7 @@
     4.4    which turns inductive specifications into equational ones, from
     4.5    which in turn executable code can be generated.  The mechanisms of
     4.6    this compiler are described in detail in
     4.7 -  \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}.
     4.8 +  @{cite "Berghofer-Bulwahn-Haftmann:2009:TPHOL"}.
     4.9  
    4.10    Consider the simple predicate @{const append} given by these two
    4.11    introduction rules:
     5.1 --- a/src/Doc/Codegen/Introduction.thy	Tue Oct 07 21:44:41 2014 +0200
     5.2 +++ b/src/Doc/Codegen/Introduction.thy	Tue Oct 07 22:35:11 2014 +0200
     5.3 @@ -8,12 +8,12 @@
     5.4    This tutorial introduces the code generator facilities of @{text
     5.5    "Isabelle/HOL"}.  It allows to turn (a certain class of) HOL
     5.6    specifications into corresponding executable code in the programming
     5.7 -  languages @{text SML} \cite{SML}, @{text OCaml} \cite{OCaml},
     5.8 -  @{text Haskell} \cite{haskell-revised-report} and @{text Scala}
     5.9 -  \cite{scala-overview-tech-report}.
    5.10 +  languages @{text SML} @{cite SML}, @{text OCaml} @{cite OCaml},
    5.11 +  @{text Haskell} @{cite "haskell-revised-report"} and @{text Scala}
    5.12 +  @{cite "scala-overview-tech-report"}.
    5.13  
    5.14    To profit from this tutorial, some familiarity and experience with
    5.15 -  @{theory HOL} \cite{isa-tutorial} and its basic theories is assumed.
    5.16 +  @{theory HOL} @{cite "isa-tutorial"} and its basic theories is assumed.
    5.17  *}
    5.18  
    5.19  
    5.20 @@ -28,7 +28,7 @@
    5.21    a generated program as an implementation of a higher-order rewrite
    5.22    system, then every rewrite step performed by the program can be
    5.23    simulated in the logic, which guarantees partial correctness
    5.24 -  \cite{Haftmann-Nipkow:2010:code}.
    5.25 +  @{cite "Haftmann-Nipkow:2010:code"}.
    5.26  *}
    5.27  
    5.28  
    5.29 @@ -221,11 +221,11 @@
    5.30      \item You may want to skim over the more technical sections
    5.31        \secref{sec:adaptation} and \secref{sec:further}.
    5.32  
    5.33 -    \item The target language Scala \cite{scala-overview-tech-report}
    5.34 +    \item The target language Scala @{cite "scala-overview-tech-report"}
    5.35        comes with some specialities discussed in \secref{sec:scala}.
    5.36  
    5.37      \item For exhaustive syntax diagrams etc. you should visit the
    5.38 -      Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}.
    5.39 +      Isabelle/Isar Reference Manual @{cite "isabelle-isar-ref"}.
    5.40  
    5.41    \end{itemize}
    5.42  
     6.1 --- a/src/Doc/Codegen/Refinement.thy	Tue Oct 07 21:44:41 2014 +0200
     6.2 +++ b/src/Doc/Codegen/Refinement.thy	Tue Oct 07 22:35:11 2014 +0200
     6.3 @@ -264,7 +264,7 @@
     6.4  *}
     6.5  
     6.6  text {*
     6.7 -  See further \cite{Haftmann-Kraus-Kuncar-Nipkow:2013:data_refinement}
     6.8 +  See further @{cite "Haftmann-Kraus-Kuncar-Nipkow:2013:data_refinement"}
     6.9    for the meta theory of datatype refinement involving invariants.
    6.10  
    6.11    Typical data structures implemented by representations involving
     7.1 --- a/src/Doc/Datatypes/Datatypes.thy	Tue Oct 07 21:44:41 2014 +0200
     7.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Tue Oct 07 22:35:11 2014 +0200
     7.3 @@ -23,7 +23,7 @@
     7.4  text {*
     7.5  The 2013 edition of Isabelle introduced a definitional package for freely
     7.6  generated datatypes and codatatypes. This package replaces the earlier
     7.7 -implementation due to Berghofer and Wenzel \cite{Berghofer-Wenzel:1999:TPHOL}.
     7.8 +implementation due to Berghofer and Wenzel @{cite "Berghofer-Wenzel:1999:TPHOL"}.
     7.9  Perhaps the main advantage of the new package is that it supports recursion
    7.10  through a large class of non-datatypes, such as finite sets:
    7.11  *}
    7.12 @@ -80,13 +80,14 @@
    7.13  \verb|~~/src/HOL/Library|.
    7.14  
    7.15  The package, like its predecessor, fully adheres to the LCF philosophy
    7.16 -\cite{mgordon79}: The characteristic theorems associated with the specified
    7.17 +@{cite mgordon79}: The characteristic theorems associated with the specified
    7.18  (co)datatypes are derived rather than introduced axiomatically.%
    7.19  \footnote{However, some of the
    7.20  internal constructions and most of the internal proof obligations are omitted
    7.21  if the @{text quick_and_dirty} option is enabled.}
    7.22  The package is described in a number of papers
    7.23 -\cite{traytel-et-al-2012,blanchette-et-al-wit,blanchette-et-al-2014-impl,panny-et-al-2014}.
    7.24 +@{cite "traytel-et-al-2012" and "blanchette-et-al-wit" and
    7.25 +  "blanchette-et-al-2014-impl" and "panny-et-al-2014"}.
    7.26  The central notion is that of a \emph{bounded natural functor} (BNF)---a
    7.27  well-behaved type constructor for which nested (co)recursion is supported.
    7.28  
    7.29 @@ -488,7 +489,7 @@
    7.30  datatypes specified by their constructors.
    7.31  
    7.32  The syntactic entity \synt{target} can be used to specify a local
    7.33 -context (e.g., @{text "(in linorder)"} \cite{isabelle-isar-ref}),
    7.34 +context (e.g., @{text "(in linorder)"} @{cite "isabelle-isar-ref"}),
    7.35  and \synt{prop} denotes a HOL proposition.
    7.36  
    7.37  The optional target is optionally followed by a combination of the following
    7.38 @@ -527,7 +528,7 @@
    7.39  \noindent
    7.40  The syntactic entity \synt{name} denotes an identifier, \synt{mixfix} denotes
    7.41  the usual parenthesized mixfix notation, and \synt{typefree} denotes fixed type
    7.42 -variable (@{typ 'a}, @{typ 'b}, \ldots) \cite{isabelle-isar-ref}.
    7.43 +variable (@{typ 'a}, @{typ 'b}, \ldots) @{cite "isabelle-isar-ref"}.
    7.44  
    7.45  The optional names preceding the type variables allow to override the default
    7.46  names of the set functions (@{text set\<^sub>1_t}, \ldots, @{text set\<^sub>m_t}). Type
    7.47 @@ -561,7 +562,7 @@
    7.48  \medskip
    7.49  
    7.50  \noindent
    7.51 -The syntactic entity \synt{type} denotes a HOL type \cite{isabelle-isar-ref}.
    7.52 +The syntactic entity \synt{type} denotes a HOL type @{cite "isabelle-isar-ref"}.
    7.53  
    7.54  In addition to the type of a constructor argument, it is possible to specify a
    7.55  name for the corresponding selector to override the default name
    7.56 @@ -596,7 +597,7 @@
    7.57      ML {* Old_Datatype_Data.get_info @{theory} @{type_name even_nat} *}
    7.58  
    7.59  text {*
    7.60 -The syntactic entity \synt{name} denotes an identifier \cite{isabelle-isar-ref}.
    7.61 +The syntactic entity \synt{name} denotes an identifier @{cite "isabelle-isar-ref"}.
    7.62  
    7.63  The command can be useful because the old datatype package provides some
    7.64  functionality that is not yet replicated in the new package.
    7.65 @@ -1121,7 +1122,7 @@
    7.66  command, which supports primitive recursion, or using the more general
    7.67  \keyw{fun} and \keyw{function} commands. Here, the focus is on
    7.68  @{command primrec}; the other two commands are described in a separate
    7.69 -tutorial \cite{isabelle-function}.
    7.70 +tutorial @{cite "isabelle-function"}.
    7.71  
    7.72  %%% TODO: partial_function
    7.73  *}
    7.74 @@ -1473,7 +1474,7 @@
    7.75  The syntactic entity \synt{target} can be used to specify a local context,
    7.76  \synt{fixes} denotes a list of names with optional type signatures,
    7.77  \synt{thmdecl} denotes an optional name for the formula that follows, and
    7.78 -\synt{prop} denotes a HOL proposition \cite{isabelle-isar-ref}.
    7.79 +\synt{prop} denotes a HOL proposition @{cite "isabelle-isar-ref"}.
    7.80  
    7.81  The optional target is optionally followed by the following option:
    7.82  
    7.83 @@ -1606,7 +1607,7 @@
    7.84  flavors of corecursion. More examples can be found in the directory
    7.85  \verb|~~/src/HOL/|\allowbreak\verb|BNF/Examples|. The
    7.86  \emph{Archive of Formal Proofs} also includes some useful codatatypes, notably
    7.87 -for lazy lists \cite{lochbihler-2010}.
    7.88 +for lazy lists @{cite "lochbihler-2010"}.
    7.89  *}
    7.90  
    7.91  
    7.92 @@ -2408,7 +2409,7 @@
    7.93  The syntactic entity \synt{target} can be used to specify a local context,
    7.94  \synt{fixes} denotes a list of names with optional type signatures,
    7.95  \synt{thmdecl} denotes an optional name for the formula that follows, and
    7.96 -\synt{prop} denotes a HOL proposition \cite{isabelle-isar-ref}.
    7.97 +\synt{prop} denotes a HOL proposition @{cite "isabelle-isar-ref"}.
    7.98  
    7.99  The optional target is optionally followed by one or both of the following
   7.100  options:
   7.101 @@ -2468,7 +2469,7 @@
   7.102  text {*
   7.103  Bounded natural functors (BNFs) are a semantic criterion for where
   7.104  (co)re\-cur\-sion may appear on the right-hand side of an equation
   7.105 -\cite{traytel-et-al-2012,blanchette-et-al-wit}.
   7.106 +@{cite "traytel-et-al-2012" and "blanchette-et-al-wit"}.
   7.107  
   7.108  An $n$-ary BNF is a type constructor equipped with a map function
   7.109  (functorial action), $n$ set functions (natural transformations),
   7.110 @@ -2641,7 +2642,7 @@
   7.111  
   7.112  The syntactic entity \synt{target} can be used to specify a local context,
   7.113  \synt{type} denotes a HOL type, and \synt{term} denotes a HOL term
   7.114 -\cite{isabelle-isar-ref}.
   7.115 +@{cite "isabelle-isar-ref"}.
   7.116  
   7.117  %%% TODO: elaborate on proof obligations
   7.118  *}
   7.119 @@ -2673,7 +2674,7 @@
   7.120  The syntactic entity \synt{target} can be used to specify a local context,
   7.121  \synt{name} denotes an identifier, \synt{typefree} denotes fixed type variable
   7.122  (@{typ 'a}, @{typ 'b}, \ldots), and \synt{mixfix} denotes the usual
   7.123 -parenthesized mixfix notation \cite{isabelle-isar-ref}.
   7.124 +parenthesized mixfix notation @{cite "isabelle-isar-ref"}.
   7.125  
   7.126  Type arguments are live by default; they can be marked as dead by entering
   7.127  @{text dead} in front of the type variable (e.g., @{text "(dead 'a)"})
   7.128 @@ -2755,7 +2756,7 @@
   7.129  
   7.130  The syntactic entity \synt{target} can be used to specify a local context,
   7.131  \synt{name} denotes an identifier, \synt{prop} denotes a HOL proposition, and
   7.132 -\synt{term} denotes a HOL term \cite{isabelle-isar-ref}.
   7.133 +\synt{term} denotes a HOL term @{cite "isabelle-isar-ref"}.
   7.134  
   7.135  The syntax resembles that of @{command datatype} and @{command codatatype}
   7.136  definitions (Sections
     8.1 --- a/src/Doc/Functions/Functions.thy	Tue Oct 07 21:44:41 2014 +0200
     8.2 +++ b/src/Doc/Functions/Functions.thy	Tue Oct 07 22:35:11 2014 +0200
     8.3 @@ -278,7 +278,7 @@
     8.4  text {*
     8.5    To see how the automatic termination proofs work, let's look at an
     8.6    example where it fails\footnote{For a detailed discussion of the
     8.7 -  termination prover, see \cite{bulwahnKN07}}:
     8.8 +  termination prover, see @{cite bulwahnKN07}}:
     8.9  
    8.10  \end{isamarkuptext}  
    8.11  \cmd{fun} @{text "fails :: \"nat \<Rightarrow> nat list \<Rightarrow> nat\""}\\%
    8.12 @@ -334,7 +334,7 @@
    8.13    more powerful @{text size_change} method, which uses a variant of
    8.14    the size-change principle, together with some other
    8.15    techniques. While the details are discussed
    8.16 -  elsewhere\cite{krauss_phd},
    8.17 +  elsewhere @{cite krauss_phd},
    8.18    here are a few typical situations where
    8.19    @{text lexicographic_order} has difficulties and @{text size_change}
    8.20    may be worth a try:
     9.1 --- a/src/Doc/Locales/Examples.thy	Tue Oct 07 21:44:41 2014 +0200
     9.2 +++ b/src/Doc/Locales/Examples.thy	Tue Oct 07 22:35:11 2014 +0200
     9.3 @@ -295,7 +295,7 @@
     9.4    exception of the context elements \isakeyword{constrains} and
     9.5    \isakeyword{defines}, which are provided for backward
     9.6    compatibility.  See the Isabelle/Isar Reference
     9.7 -  Manual~\cite{IsarRef} for full documentation.  *}
     9.8 +  Manual @{cite IsarRef} for full documentation.  *}
     9.9  
    9.10  
    9.11  section {* Import \label{sec:import} *}
    9.12 @@ -763,7 +763,7 @@
    9.13    The sublocale relation is transitive --- that is, propagation takes
    9.14    effect along chains of sublocales.  Even cycles in the sublocale relation are
    9.15    supported, as long as these cycles do not lead to infinite chains.
    9.16 -  Details are discussed in the technical report \cite{Ballarin2006a}.
    9.17 +  Details are discussed in the technical report @{cite Ballarin2006a}.
    9.18    See also Section~\ref{sec:infinite-chains} of this tutorial.  *}
    9.19  
    9.20  end
    10.1 --- a/src/Doc/Locales/Examples3.thy	Tue Oct 07 21:44:41 2014 +0200
    10.2 +++ b/src/Doc/Locales/Examples3.thy	Tue Oct 07 22:35:11 2014 +0200
    10.3 @@ -502,13 +502,13 @@
    10.4  
    10.5  text {* More information on locales and their interpretation is
    10.6    available.  For the locale hierarchy of import and interpretation
    10.7 -  dependencies see~\cite{Ballarin2006a}; interpretations in theories
    10.8 -  and proofs are covered in~\cite{Ballarin2006b}.  In the latter, I
    10.9 +  dependencies see~@{cite Ballarin2006a}; interpretations in theories
   10.10 +  and proofs are covered in~@{cite Ballarin2006b}.  In the latter, I
   10.11    show how interpretation in proofs enables to reason about families
   10.12    of algebraic structures, which cannot be expressed with locales
   10.13    directly.
   10.14  
   10.15 -  Haftmann and Wenzel~\cite{HaftmannWenzel2007} overcome a restriction
   10.16 +  Haftmann and Wenzel~@{cite HaftmannWenzel2007} overcome a restriction
   10.17    of axiomatic type classes through a combination with locale
   10.18    interpretation.  The result is a Haskell-style class system with a
   10.19    facility to generate ML and Haskell code.  Classes are sufficient for
   10.20 @@ -520,14 +520,14 @@
   10.21    The locales reimplementation for Isabelle 2009 provides, among other
   10.22    improvements, a clean integration with Isabelle/Isar's local theory
   10.23    mechanisms, which are described in another paper by Haftmann and
   10.24 -  Wenzel~\cite{HaftmannWenzel2009}.
   10.25 +  Wenzel~@{cite HaftmannWenzel2009}.
   10.26  
   10.27 -  The original work of Kamm\"uller on locales~\cite{KammullerEtAl1999}
   10.28 +  The original work of Kamm\"uller on locales~@{cite KammullerEtAl1999}
   10.29    may be of interest from a historical perspective.  My previous
   10.30 -  report on locales and locale expressions~\cite{Ballarin2004a}
   10.31 +  report on locales and locale expressions~@{cite Ballarin2004a}
   10.32    describes a simpler form of expressions than available now and is
   10.33    outdated. The mathematical background on orders and lattices is
   10.34 -  taken from Jacobson's textbook on algebra~\cite[Chapter~8]{Jacobson1985}.
   10.35 +  taken from Jacobson's textbook on algebra~@{cite \<open>Chapter~8\<close> Jacobson1985}.
   10.36  
   10.37    The sources of this tutorial, which include all proofs, are
   10.38    available with the Isabelle distribution at
    11.1 --- a/src/Doc/Logics_ZF/ZF_Isar.thy	Tue Oct 07 21:44:41 2014 +0200
    11.2 +++ b/src/Doc/Logics_ZF/ZF_Isar.thy	Tue Oct 07 22:35:11 2014 +0200
    11.3 @@ -94,7 +94,7 @@
    11.4      hints: @{syntax (ZF) "monos"}? @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
    11.5    \<close>}
    11.6  
    11.7 -  See \cite{isabelle-ZF} for further information on inductive
    11.8 +  See @{cite "isabelle-ZF"} for further information on inductive
    11.9    definitions in ZF, but note that this covers the old-style theory
   11.10    format.
   11.11  *}
    12.1 --- a/src/Doc/Prog_Prove/Logic.thy	Tue Oct 07 21:44:41 2014 +0200
    12.2 +++ b/src/Doc/Prog_Prove/Logic.thy	Tue Oct 07 22:35:11 2014 +0200
    12.3 @@ -139,7 +139,7 @@
    12.4  @{thm image_def}\index{$IMP042@@{term"f ` A"}} & is the image of a function over a set
    12.5  \end{tabular}
    12.6  \end{center}
    12.7 -See \cite{Nipkow-Main} for the wealth of further predefined functions in theory
    12.8 +See @{cite "Nipkow-Main"} for the wealth of further predefined functions in theory
    12.9  @{theory Main}.
   12.10  
   12.11  
   12.12 @@ -399,7 +399,7 @@
   12.13    {\mbox{@{text"?P = ?Q"}}}
   12.14  \]
   12.15  These rules are part of the logical system of \concept{natural deduction}
   12.16 -(e.g., \cite{HuthRyan}). Although we intentionally de-emphasize the basic rules
   12.17 +(e.g., @{cite HuthRyan}). Although we intentionally de-emphasize the basic rules
   12.18  of logic in favour of automatic proof methods that allow you to take bigger
   12.19  steps, these rules are helpful in locating where and why automation fails.
   12.20  When applied backwards, these rules decompose the goal:
   12.21 @@ -486,7 +486,7 @@
   12.22  %
   12.23  %Command \isacom{find{\isacharunderscorekeyword}theorems} searches for specific theorems in the current
   12.24  %theory. Search criteria include pattern matching on terms and on names.
   12.25 -%For details see the Isabelle/Isar Reference Manual~\cite{IsarRef}.
   12.26 +%For details see the Isabelle/Isar Reference Manual~@{cite IsarRef}.
   12.27  %\bigskip
   12.28  
   12.29  \begin{warn}
    13.1 --- a/src/Doc/Prog_Prove/Types_and_funs.thy	Tue Oct 07 21:44:41 2014 +0200
    13.2 +++ b/src/Doc/Prog_Prove/Types_and_funs.thy	Tue Oct 07 22:35:11 2014 +0200
    13.3 @@ -148,7 +148,7 @@
    13.4  is measured as the number of constructors (excluding 0-ary ones, e.g., @{text
    13.5  Nil}). Lexicographic combinations are also recognized. In more complicated
    13.6  situations, the user may have to prove termination by hand. For details
    13.7 -see~\cite{Krauss}.
    13.8 +see~@{cite Krauss}.
    13.9  
   13.10  Functions defined with \isacom{fun} come with their own induction schema
   13.11  that mirrors the recursion schema and is derived from the termination
    14.1 --- a/src/Doc/Sugar/Sugar.thy	Tue Oct 07 21:44:41 2014 +0200
    14.2 +++ b/src/Doc/Sugar/Sugar.thy	Tue Oct 07 22:35:11 2014 +0200
    14.3 @@ -14,7 +14,7 @@
    14.4  @{thm[display,mode=latex_sum] setsum_Suc_diff[no_vars]}
    14.5  No typos, no omissions, no sweat.
    14.6  If you have not experienced that joy, read Chapter 4, \emph{Presenting
    14.7 -Theories}, \cite{LNCS2283} first.
    14.8 +Theories}, @{cite LNCS2283} first.
    14.9  
   14.10  If you have mastered the art of Isabelle's \emph{antiquotations},
   14.11  i.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity
   14.12 @@ -180,7 +180,7 @@
   14.13  \subsection{Inference rules}
   14.14  
   14.15  To print theorems as inference rules you need to include Didier
   14.16 -R\'emy's \texttt{mathpartir} package~\cite{mathpartir}
   14.17 +R\'emy's \texttt{mathpartir} package~@{cite mathpartir}
   14.18  for typesetting inference rules in your \LaTeX\ file.
   14.19  
   14.20  Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces
    15.1 --- a/src/Doc/Tutorial/Advanced/WFrec.thy	Tue Oct 07 21:44:41 2014 +0200
    15.2 +++ b/src/Doc/Tutorial/Advanced/WFrec.thy	Tue Oct 07 22:35:11 2014 +0200
    15.3 @@ -29,7 +29,7 @@
    15.4  left-hand side of an equation and $r$ the argument of some recursive call on
    15.5  the corresponding right-hand side, induces a well-founded relation.  For a
    15.6  systematic account of termination proofs via well-founded relations see, for
    15.7 -example, Baader and Nipkow~\cite{Baader-Nipkow}.
    15.8 +example, Baader and Nipkow~@{cite "Baader-Nipkow"}.
    15.9  
   15.10  Each \isacommand{recdef} definition should be accompanied (after the function's
   15.11  name) by a well-founded relation on the function's argument type.  
    16.1 --- a/src/Doc/Tutorial/Advanced/simp2.thy	Tue Oct 07 21:44:41 2014 +0200
    16.2 +++ b/src/Doc/Tutorial/Advanced/simp2.thy	Tue Oct 07 22:35:11 2014 +0200
    16.3 @@ -123,7 +123,7 @@
    16.4  rewrite rules. This is not quite true.  For reasons of feasibility,
    16.5  the simplifier expects the
    16.6  left-hand side of each rule to be a so-called \emph{higher-order
    16.7 -pattern}~\cite{nipkow-patterns}\indexbold{patterns!higher-order}. 
    16.8 +pattern}~@{cite "nipkow-patterns"}\indexbold{patterns!higher-order}. 
    16.9  This restricts where
   16.10  unknowns may occur.  Higher-order patterns are terms in $\beta$-normal
   16.11  form.  (This means there are no subterms of the form $(\lambda x. M)(N)$.)  
    17.1 --- a/src/Doc/Tutorial/CTL/Base.thy	Tue Oct 07 21:44:41 2014 +0200
    17.2 +++ b/src/Doc/Tutorial/CTL/Base.thy	Tue Oct 07 22:35:11 2014 +0200
    17.3 @@ -7,7 +7,7 @@
    17.4  Computation Tree Logic (CTL), a temporal logic.
    17.5  Model checking is a popular technique for the verification of finite
    17.6  state systems (implementations) with respect to temporal logic formulae
    17.7 -(specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are set theoretic
    17.8 +(specifications) @{cite "ClarkeGP-book" and "Huth-Ryan-book"}. Its foundations are set theoretic
    17.9  and this section will explore them in HOL\@. This is done in two steps.  First
   17.10  we consider a simple modal logic called propositional dynamic
   17.11  logic (PDL)\@.  We then proceed to the temporal logic CTL, which is
    18.1 --- a/src/Doc/Tutorial/CTL/CTL.thy	Tue Oct 07 21:44:41 2014 +0200
    18.2 +++ b/src/Doc/Tutorial/CTL/CTL.thy	Tue Oct 07 22:35:11 2014 +0200
    18.3 @@ -361,7 +361,7 @@
    18.4  %{text[display]"| EU formula formula    E[_ U _]"}
    18.5  %which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.
    18.6  \end{exercise}
    18.7 -For more CTL exercises see, for example, Huth and Ryan \cite{Huth-Ryan-book}.
    18.8 +For more CTL exercises see, for example, Huth and Ryan @{cite "Huth-Ryan-book"}.
    18.9  *}
   18.10  
   18.11  (*<*)
   18.12 @@ -439,7 +439,7 @@
   18.13  our model checkers.  It is clear that if all sets are finite, they can be
   18.14  represented as lists and the usual set operations are easily
   18.15  implemented. Only @{const lfp} requires a little thought.  Fortunately, theory
   18.16 -@{text While_Combinator} in the Library~\cite{HOL-Library} provides a
   18.17 +@{text While_Combinator} in the Library~@{cite "HOL-Library"} provides a
   18.18  theorem stating that in the case of finite sets and a monotone
   18.19  function~@{term F}, the value of \mbox{@{term"lfp F"}} can be computed by
   18.20  iterated application of @{term F} to~@{term"{}"} until a fixed point is
    19.1 --- a/src/Doc/Tutorial/CTL/PDL.thy	Tue Oct 07 21:44:41 2014 +0200
    19.2 +++ b/src/Doc/Tutorial/CTL/PDL.thy	Tue Oct 07 22:35:11 2014 +0200
    19.3 @@ -8,7 +8,7 @@
    19.4  connectives @{text AX} and @{text EF}\@. Since formulae are essentially
    19.5  syntax trees, they are naturally modelled as a datatype:%
    19.6  \footnote{The customary definition of PDL
    19.7 -\cite{HarelKT-DL} looks quite different from ours, but the two are easily
    19.8 +@{cite "HarelKT-DL"} looks quite different from ours, but the two are easily
    19.9  shown to be equivalent.}
   19.10  *}
   19.11  
    20.1 --- a/src/Doc/Tutorial/Datatype/Nested.thy	Tue Oct 07 21:44:41 2014 +0200
    20.2 +++ b/src/Doc/Tutorial/Datatype/Nested.thy	Tue Oct 07 22:35:11 2014 +0200
    20.3 @@ -150,7 +150,7 @@
    20.4  instead.  Simple uses of \isacommand{fun} are described in
    20.5  \S\ref{sec:fun} below.  Advanced applications, including functions
    20.6  over nested datatypes like @{text term}, are discussed in a
    20.7 -separate tutorial~\cite{isabelle-function}.
    20.8 +separate tutorial~@{cite "isabelle-function"}.
    20.9  
   20.10  Of course, you may also combine mutual and nested recursion of datatypes. For example,
   20.11  constructor @{text Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
    21.1 --- a/src/Doc/Tutorial/Documents/Documents.thy	Tue Oct 07 21:44:41 2014 +0200
    21.2 +++ b/src/Doc/Tutorial/Documents/Documents.thy	Tue Oct 07 22:35:11 2014 +0200
    21.3 @@ -11,7 +11,7 @@
    21.4    for the parser and output templates for the pretty printer.
    21.5  
    21.6    In full generality, parser and pretty printer configuration is a
    21.7 -  subtle affair~\cite{isabelle-isar-ref}.  Your syntax specifications need
    21.8 +  subtle affair~@{cite "isabelle-isar-ref"}.  Your syntax specifications need
    21.9    to interact properly with the existing setup of Isabelle/Pure and
   21.10    Isabelle/HOL\@.  To avoid creating ambiguities with existing
   21.11    elements, it is particularly important to give new syntactic
   21.12 @@ -107,7 +107,7 @@
   21.13    \verb,\,\verb,<forall>, symbol as~@{text \<forall>}.
   21.14  
   21.15    A list of standard Isabelle symbols is given in
   21.16 -  \cite{isabelle-isar-ref}.  You may introduce your own
   21.17 +  @{cite "isabelle-isar-ref"}.  You may introduce your own
   21.18    interpretation of further symbols by configuring the appropriate
   21.19    front-end tool accordingly, e.g.\ by defining certain {\LaTeX}
   21.20    macros (see also \S\ref{sec:doc-prep-symbols}).  There are also a
   21.21 @@ -153,7 +153,7 @@
   21.22    be displayed after further input.
   21.23  
   21.24    More flexible is to provide alternative syntax forms
   21.25 -  through the \bfindex{print mode} concept~\cite{isabelle-isar-ref}.  By
   21.26 +  through the \bfindex{print mode} concept~@{cite "isabelle-isar-ref"}.  By
   21.27    convention, the mode of ``$xsymbols$'' is enabled whenever
   21.28    Proof~General's X-Symbol mode or {\LaTeX} output is active.  Now
   21.29    consider the following hybrid declaration of @{text xor}:
   21.30 @@ -187,7 +187,7 @@
   21.31  
   21.32  text {*
   21.33    Prefix syntax annotations\index{prefix annotation} are another form
   21.34 -  of mixfixes \cite{isabelle-isar-ref}, without any template arguments or
   21.35 +  of mixfixes @{cite "isabelle-isar-ref"}, without any template arguments or
   21.36    priorities --- just some literal syntax.  The following example
   21.37    associates common symbols with the constructors of a datatype.
   21.38  *}
   21.39 @@ -262,7 +262,7 @@
   21.40  
   21.41  Abbreviations are a simplified form of the general concept of
   21.42  \emph{syntax translations}; even heavier transformations may be
   21.43 -written in ML \cite{isabelle-isar-ref}.
   21.44 +written in ML @{cite "isabelle-isar-ref"}.
   21.45  *}
   21.46  
   21.47  
   21.48 @@ -351,7 +351,7 @@
   21.49    setup) and \texttt{isabelle build} (to run sessions as specified in
   21.50    the corresponding \texttt{ROOT} file).  These Isabelle tools are
   21.51    described in further detail in the \emph{Isabelle System Manual}
   21.52 -  \cite{isabelle-sys}.
   21.53 +  @{cite "isabelle-sys"}.
   21.54  
   21.55    For example, a new session \texttt{MySession} (with document
   21.56    preparation) may be produced as follows:
   21.57 @@ -412,7 +412,7 @@
   21.58    \texttt{MySession/document} directory as well.  In particular,
   21.59    adding a file named \texttt{root.bib} causes an automatic run of
   21.60    \texttt{bibtex} to process a bibliographic database; see also
   21.61 -  \texttt{isabelle document} \cite{isabelle-sys}.
   21.62 +  \texttt{isabelle document} @{cite "isabelle-sys"}.
   21.63  
   21.64    \medskip Any failure of the document preparation phase in an
   21.65    Isabelle batch session leaves the generated sources in their target
   21.66 @@ -526,7 +526,7 @@
   21.67    theory or proof context (\bfindex{text blocks}).
   21.68  
   21.69    \medskip Marginal comments are part of each command's concrete
   21.70 -  syntax \cite{isabelle-isar-ref}; the common form is ``\verb,--,~$text$''
   21.71 +  syntax @{cite "isabelle-isar-ref"}; the common form is ``\verb,--,~$text$''
   21.72    where $text$ is delimited by \verb,",@{text \<dots>}\verb,", or
   21.73    \verb,{,\verb,*,~@{text \<dots>}~\verb,*,\verb,}, as before.  Multiple
   21.74    marginal comments may be given at the same time.  Here is a simple
   21.75 @@ -612,7 +612,7 @@
   21.76    same types as they have in the main goal statement.
   21.77  
   21.78    \medskip Several further kinds of antiquotations and options are
   21.79 -  available \cite{isabelle-isar-ref}.  Here are a few commonly used
   21.80 +  available @{cite "isabelle-isar-ref"}.  Here are a few commonly used
   21.81    combinations:
   21.82  
   21.83    \medskip
   21.84 @@ -661,7 +661,7 @@
   21.85    straightforward generalization of ASCII characters.  While Isabelle
   21.86    does not impose any interpretation of the infinite collection of
   21.87    named symbols, {\LaTeX} documents use canonical glyphs for certain
   21.88 -  standard symbols \cite{isabelle-isar-ref}.
   21.89 +  standard symbols @{cite "isabelle-isar-ref"}.
   21.90  
   21.91    The {\LaTeX} code produced from Isabelle text follows a simple
   21.92    scheme.  You can tune the final appearance by redefining certain
   21.93 @@ -751,7 +751,7 @@
   21.94    preparation system allows the user to specify how to interpret a
   21.95    tagged region, in order to keep, drop, or fold the corresponding
   21.96    parts of the document.  See the \emph{Isabelle System Manual}
   21.97 -  \cite{isabelle-sys} for further details, especially on
   21.98 +  @{cite "isabelle-sys"} for further details, especially on
   21.99    \texttt{isabelle build} and \texttt{isabelle document}.
  21.100  
  21.101    Ignored material is specified by delimiting the original formal
    22.1 --- a/src/Doc/Tutorial/Fun/fun0.thy	Tue Oct 07 21:44:41 2014 +0200
    22.2 +++ b/src/Doc/Tutorial/Fun/fun0.thy	Tue Oct 07 22:35:11 2014 +0200
    22.3 @@ -96,7 +96,7 @@
    22.4  
    22.5  text{* The order of arguments has no influence on whether
    22.6  \isacommand{fun} can prove termination of a function. For more details
    22.7 -see elsewhere~\cite{bulwahnKN07}.
    22.8 +see elsewhere~@{cite bulwahnKN07}.
    22.9  
   22.10  \subsection{Simplification}
   22.11  \label{sec:fun-simplification}
    23.1 --- a/src/Doc/Tutorial/Inductive/AB.thy	Tue Oct 07 21:44:41 2014 +0200
    23.2 +++ b/src/Doc/Tutorial/Inductive/AB.thy	Tue Oct 07 22:35:11 2014 +0200
    23.3 @@ -17,7 +17,7 @@
    23.4  B &\to& b S \mid a B B \nonumber
    23.5  \end{eqnarray}
    23.6  At the end we say a few words about the relationship between
    23.7 -the original proof \cite[p.\ts81]{HopcroftUllman} and our formal version.
    23.8 +the original proof @{cite \<open>p.\ts81\<close> HopcroftUllman} and our formal version.
    23.9  
   23.10  We start by fixing the alphabet, which consists only of @{term a}'s
   23.11  and~@{term b}'s:
   23.12 @@ -283,7 +283,7 @@
   23.13  text{*
   23.14  We conclude this section with a comparison of our proof with 
   23.15  Hopcroft\index{Hopcroft, J. E.} and Ullman's\index{Ullman, J. D.}
   23.16 -\cite[p.\ts81]{HopcroftUllman}.
   23.17 +@{cite \<open>p.\ts81\<close> HopcroftUllman}.
   23.18  For a start, the textbook
   23.19  grammar, for no good reason, excludes the empty word, thus complicating
   23.20  matters just a little bit: they have 8 instead of our 7 productions.
    24.1 --- a/src/Doc/Tutorial/Protocol/NS_Public.thy	Tue Oct 07 21:44:41 2014 +0200
    24.2 +++ b/src/Doc/Tutorial/Protocol/NS_Public.thy	Tue Oct 07 22:35:11 2014 +0200
    24.3 @@ -381,8 +381,8 @@
    24.4  \medskip
    24.5  
    24.6  Detailed information on this protocol verification technique can be found
    24.7 -elsewhere~\cite{paulson-jcs}, including proofs of an Internet
    24.8 -protocol~\cite{paulson-tls}.  We must stress that the protocol discussed
    24.9 +elsewhere~@{cite "paulson-jcs"}, including proofs of an Internet
   24.10 +protocol~@{cite "paulson-tls"}.  We must stress that the protocol discussed
   24.11  in this chapter is trivial.  There are only three messages; no keys are
   24.12  exchanged; we merely have to prove that encrypted data remains secret. 
   24.13  Real world protocols are much longer and distribute many secrets to their
   24.14 @@ -391,7 +391,7 @@
   24.15  been used to encrypt other sensitive information, there may be cascading
   24.16  losses.  We may still be able to establish a bound on the losses and to
   24.17  prove that other protocol runs function
   24.18 -correctly~\cite{paulson-yahalom}.  Proofs of real-world protocols follow
   24.19 +correctly~@{cite "paulson-yahalom"}.  Proofs of real-world protocols follow
   24.20  the strategy illustrated above, but the subgoals can
   24.21  be much bigger and there are more of them.
   24.22  \index{protocols!security|)}
    25.1 --- a/src/Doc/Tutorial/Types/Axioms.thy	Tue Oct 07 21:44:41 2014 +0200
    25.2 +++ b/src/Doc/Tutorial/Types/Axioms.thy	Tue Oct 07 22:35:11 2014 +0200
    25.3 @@ -8,7 +8,7 @@
    25.4  
    25.5  \begin{warn}
    25.6  Proofs in this section use structured \emph{Isar} proofs, which are not
    25.7 -covered in this tutorial; but see \cite{Nipkow-TYPES02}.%
    25.8 +covered in this tutorial; but see @{cite "Nipkow-TYPES02"}.%
    25.9  \end{warn} *}
   25.10  
   25.11  subsubsection {* Semigroups *}
    26.1 --- a/src/Doc/Tutorial/Types/Records.thy	Tue Oct 07 21:44:41 2014 +0200
    26.2 +++ b/src/Doc/Tutorial/Types/Records.thy	Tue Oct 07 22:35:11 2014 +0200
    26.3 @@ -33,7 +33,7 @@
    26.4  
    26.5  text {*
    26.6    Record types are not primitive in Isabelle and have a delicate
    26.7 -  internal representation \cite{NaraschewskiW-TPHOLs98}, based on
    26.8 +  internal representation @{cite "NaraschewskiW-TPHOLs98"}, based on
    26.9    nested copies of the primitive product type.  A \commdx{record}
   26.10    declaration introduces a new record type scheme by specifying its
   26.11    fields, which are packaged internally to hold up the perception of
    27.1 --- a/src/Doc/Tutorial/Types/Typedefs.thy	Tue Oct 07 21:44:41 2014 +0200
    27.2 +++ b/src/Doc/Tutorial/Types/Typedefs.thy	Tue Oct 07 22:35:11 2014 +0200
    27.3 @@ -216,7 +216,7 @@
    27.4  example to demonstrate \isacommand{typedef} because its simplicity makes the
    27.5  key concepts particularly easy to grasp. If you would like to see a
    27.6  non-trivial example that cannot be defined more directly, we recommend the
    27.7 -definition of \emph{finite multisets} in the Library~\cite{HOL-Library}.
    27.8 +definition of \emph{finite multisets} in the Library~@{cite "HOL-Library"}.
    27.9  
   27.10  Let us conclude by summarizing the above procedure for defining a new type.
   27.11  Given some abstract axiomatic description $P$ of a type $ty$ in terms of a