src/Doc/Implementation/Syntax.thy

   an adequate foundation for logical languages --- in the tradition of
   \emph{higher-order abstract syntax} --- 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{inner
   syntax} in Isabelle jargon, as opposed to the \emph{outer syntax} of
-  the theory and proof language \cite{isabelle-isar-ref}.
-
-  For example, according to \cite{church40} quantifiers are represented as
+  the theory and proof language @{cite "isabelle-isar-ref"}.
+
+  For example, according to @{cite church40} quantifiers are represented as
   higher-order constants @{text "All :: ('a \<Rightarrow> bool) \<Rightarrow> bool"} such that @{text
   "All (\<lambda>x::'a. B x)"} faithfully represents the idea that is displayed in
   Isabelle as @{text "\<forall>x::'a. B x"} via @{keyword "binder"} notation.
-  Moreover, type-inference in the style of Hindley-Milner \cite{hindleymilner}
+  Moreover, type-inference in the style of Hindley-Milner @{cite hindleymilner}
   (and extensions) enables users to write @{text "\<forall>x. B x"} concisely, when
   the type @{text "'a"} is already clear from the
   context.\footnote{Type-inference taken to the extreme can easily confuse
   users. Beginners often stumble over unexpectedly general types inferred by
   the system.}

   @{ML Syntax.read_term}, @{ML Syntax.read_prop}, and @{ML
   Syntax.string_of_term} are the most important operations in practice.
 
   \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, nor try to analyze the output strings. Conceptually this is
-  an abstract datatype, encoded as concrete string for historical reasons.
+  Prover IDE @{cite "isabelle-jedit"}. 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.
 
   The standard way to provide the required position markup for input works via
   the outer syntax parser wrapper @{ML Parse.inner_syntax}, which is already
   part of @{ML Parse.typ}, @{ML Parse.term}, @{ML Parse.prop}. So a string
   obtained from one of the latter may be directly passed to the corresponding

   Actual parsing is based on traditional lexical analysis and Earley parsing
   for arbitrary context-free grammars. The user can specify the grammar
   declaratively via mixfix annotations. Moreover, there are \emph{syntax
   translations} 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, according to name
-  spaces for types, term variables and constants determined by the context.
+  parse_translation}, @{command print_translation} @{cite
+  "isabelle-isar-ref"}. The final scope-resolution is performed by the system,
+  according to name spaces for types, term variables and constants determined
+  by the context.
 *}
 
 text %mlref {*
   \begin{mldecls}
   @{index_ML Syntax.parse_typ: "Proof.context -> string -> typ"} \\

   ``type-improvement'', not just type-checking in the narrow sense.
   The \emph{uncheck} phase is roughly 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 "isabelle-isar-ref"}. Here the user specifies
   syntactic definitions that are managed by the system as polymorphic @{text
   "let"} bindings. These are expanded during the @{text "check"} phase, and
   contracted during the @{text "uncheck"} phase, without affecting the
   type-assignment of the given terms.
 

   For example, the @{command class} command defines a context where
   @{text "check"} 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}.
+  certain locale parameters.  See also @{cite "Haftmann-Wenzel:2009"}.
 *}
 
 text %mlref {*
   \begin{mldecls}
   @{index_ML Syntax.check_typs: "Proof.context -> typ list -> typ list"} \\