src/Doc/Implementation/Logic.thy

 chapter {* Primitive logic \label{ch:logic} *}
 
 text {*
   The logical foundations of Isabelle/Isar are that of the Pure logic,
   which has been introduced as a Natural Deduction framework in
-  \cite{paulson700}.  This is essentially the same logic as ``@{text
+  @{cite paulson700}.  This is essentially the same logic as ``@{text
   "\<lambda>HOL"}'' in the more abstract setting of Pure Type Systems (PTS)
-  \cite{Barendregt-Geuvers:2001}, although there are some key
+  @{cite "Barendregt-Geuvers:2001"}, although there are some key
   differences in the specific treatment of simple types in
   Isabelle/Pure.
 
   Following type-theoretic parlance, the Pure logic consists of three
   levels of @{text "\<lambda>"}-calculus with corresponding arrows, @{text

   vector of argument sorts @{text "(s\<^sub>1, \<dots>, s\<^sub>k)"} such
   that a type scheme @{text "(\<alpha>\<^bsub>s\<^sub>1\<^esub>, \<dots>,
   \<alpha>\<^bsub>s\<^sub>k\<^esub>)\<kappa>"} is of sort @{text "s"}.
   Consequently, type unification has most general solutions (modulo
   equivalence of sorts), so type-inference produces primary types as
-  expected \cite{nipkow-prehofer}.
+  expected @{cite "nipkow-prehofer"}.
 *}
 
 text %mlref {*
   \begin{mldecls}
   @{index_ML_type class: string} \\

 
 section {* Terms \label{sec:terms} *}
 
 text {*
   The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
-  with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}
-  or \cite{paulson-ml2}), with the types being determined by the
+  with de-Bruijn indices for bound variables (cf.\ @{cite debruijn72}
+  or @{cite "paulson-ml2"}), with the types being determined by the
   corresponding binders.  In contrast, free variables and constants
   have an explicit name and type in each occurrence.
 
   \medskip A \emph{bound variable} is a natural number @{text "b"},
   which accounts for the number of intermediate binders between the

   are irrelevant in the Pure logic, though; they cannot 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 @{text
   "\<lambda>"}-calculus become explicit: @{text "\<Rightarrow>"} for terms, and @{text
-  "\<And>/\<Longrightarrow>"} for proofs (cf.\ \cite{Berghofer-Nipkow:2000:TPHOL}).
+  "\<And>/\<Longrightarrow>"} for proofs (cf.\ @{cite "Berghofer-Nipkow:2000:TPHOL"}).
 
   Observe that locally fixed parameters (as in @{text
   "\<And>\<hyphen>intro"}) need not be recorded in the hypotheses, because
   the simple syntactic types of Pure are always inhabitable.
   ``Assumptions'' @{text "x :: \<tau>"} for type-membership are only
   present as long as some @{text "x\<^sub>\<tau>"} occurs in the statement
   body.\footnote{This is the key difference to ``@{text "\<lambda>HOL"}'' in
-  the PTS framework \cite{Barendregt-Geuvers:2001}, where hypotheses
+  the PTS framework @{cite "Barendregt-Geuvers:2001"}, where hypotheses
   @{text "x : A"} are treated uniformly for propositions and types.}
 
   \medskip The axiomatization of a theory is implicitly closed by
   forming all instances of type and term variables: @{text "\<turnstile>
   A\<vartheta>"} holds for any substitution instance of an axiom

   distinct variables @{text "\<^vec>\<alpha>"}).  The RHS may mention
   previously defined constants as above, or arbitrary constants @{text
   "d(\<alpha>\<^sub>i)"} for some @{text "\<alpha>\<^sub>i"} projected from @{text
   "\<^vec>\<alpha>"}.  Thus overloaded definitions essentially work by
   primitive recursion over the syntactic structure of a single type
-  argument.  See also \cite[\S4.3]{Haftmann-Wenzel:2006:classes}.
+  argument.  See also @{cite \<open>\S4.3\<close> "Haftmann-Wenzel:2006:classes"}.
 *}
 
 text %mlref {*
   \begin{mldecls}
   @{index_ML Logic.all: "term -> term -> term"} \\

 
 subsection {* Hereditary Harrop Formulae *}
 
 text {*
   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{extensions91}.  The most basic
+  inferences in the style of Gentzen @{cite "Gentzen:1935"}, but we allow
+  arbitrary nesting similar to @{cite extensions91}.  The most basic
   rule format is that of a \emph{Horn Clause}:
   \[
   \infer{@{text "A"}}{@{text "A\<^sub>1"} & @{text "\<dots>"} & @{text "A\<^sub>n"}}
   \]
   where @{text "A, A\<^sub>1, \<dots>, A\<^sub>n"} are atomic propositions

   \]
 
   Nesting of rules means that the positions of @{text "A\<^sub>i"} may
   again hold compound rules, not just atomic propositions.
   Propositions of this format are called \emph{Hereditary Harrop
-  Formulae} in the literature \cite{Miller:1991}.  Here we give an
+  Formulae} in the literature @{cite "Miller:1991"}.  Here we give an
   inductive characterization as follows:
 
   \medskip
   \begin{tabular}{ll}
   @{text "\<^bold>x"} & set of variables \\

   syntactic terms, two more layers of @{text "\<lambda>"}-calculus are added,
   which correspond to @{text "\<And>x :: \<alpha>. B x"} and @{text "A \<Longrightarrow> B"}
   according to the propositions-as-types principle.  The resulting
   3-level @{text "\<lambda>"}-calculus resembles ``@{text "\<lambda>HOL"}'' in the
   more abstract setting of Pure Type Systems (PTS)
-  \cite{Barendregt-Geuvers:2001}, if some fine points like schematic
+  @{cite "Barendregt-Geuvers:2001"}, if some fine points like schematic
   polymorphism and type classes are ignored.
 
   \medskip\emph{Proof abstractions} of the form @{text "\<^bold>\<lambda>x :: \<alpha>. prf"}
   or @{text "\<^bold>\<lambda>p : A. prf"} correspond to introduction of @{text
   "\<And>"}/@{text "\<Longrightarrow>"}, and \emph{proof applications} of the form @{text

   terms, all term and type labels of proof abstractions, and some
   argument terms of applications @{text "p \<cdot> t"} (if possible).
 
   There are separate operations to reconstruct the full proof term
   later on, using \emph{higher-order pattern unification}
-  \cite{nipkow-patterns,Berghofer-Nipkow:2000:TPHOL}.
+  @{cite "nipkow-patterns" and "Berghofer-Nipkow:2000:TPHOL"}.
 
   The \emph{proof checker} expects a fully reconstructed proof term,
   and can turn it into a theorem by replaying its primitive inferences
   within the kernel.  *}
 
 
 subsection {* Concrete syntax of proof terms *}
 
 text {* The concrete syntax of proof terms is a slight extension of
-  the regular inner syntax of Isabelle/Pure \cite{isabelle-isar-ref}.
+  the regular inner syntax of Isabelle/Pure @{cite "isabelle-isar-ref"}.
   Its main syntactic category @{syntax (inner) proof} is defined as
   follows:
 
   \begin{center}
   \begin{supertabular}{rclr}