src/Doc/Implementation/Syntax.thy

   Pure \<open>\<lambda>\<close>-calculus as introduced in \chref{ch:logic} is an adequate
   foundation for logical languages --- in the tradition of \<^emph>\<open>higher-order
   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"}.
-
-  For example, according to @{cite church40} quantifiers are represented as
+  syntax\<close> of the theory and proof language \<^cite>\<open>"isabelle-isar-ref"\<close>.
+
+  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
   system.\<close>
 

 
   \<^ML>\<open>Syntax.read_term\<close>, \<^ML>\<open>Syntax.read_prop\<close>, and \<^ML>\<open>Syntax.string_of_term\<close> 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,
+  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.
 
   The standard way to provide the required position markup for input works via
   the outer syntax parser wrapper \<^ML>\<open>Parse.inner_syntax\<close>, which is already

   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>\<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>
 
 text %mlref \<open>

   of ``type-inference'' or ``type-reconstruction'' or ``type-improvement'',
   not just type-checking in the narrow sense. The \<^emph>\<open>uncheck\<close> 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>\<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
   terms.
 

 
   For example, the @{command class} command defines a context where \<open>check\<close>
   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>
   \begin{mldecls}
   @{define_ML Syntax.check_typs: "Proof.context -> typ list -> typ list"} \\