# HG changeset patch
# User wenzelm
# Date 1446658367 -3600
# Node ID ddb3ac3fef45b1d475ce28422241cfb5a651d8d5
# Parent  9c50eb3bff5031102b24335d71d7db252d99bf4c
more antiquotations;

diff -r 9c50eb3bff50 -r ddb3ac3fef45 src/Doc/Implementation/Isar.thy
--- a/src/Doc/Implementation/Isar.thy	Wed Nov 04 18:14:28 2015 +0100
+++ b/src/Doc/Implementation/Isar.thy	Wed Nov 04 18:32:47 2015 +0100
@@ -183,10 +183,10 @@
   method space, e.g.\ @{method rule_tac}.
 
   \<^item> A non-trivial method always needs to make progress: an
-  identical follow-up goal state has to be avoided.\footnote{This
+  identical follow-up goal state has to be avoided.\<^footnote>\<open>This
   enables the user to write method expressions like \<open>meth\<^sup>+\<close>
   without looping, while the trivial do-nothing case can be recovered
-  via \<open>meth\<^sup>?\<close>.}
+  via \<open>meth\<^sup>?\<close>.\<close>
 
   Exception: trivial stuttering steps, such as ``@{method -}'' or
   @{method succeed}.
@@ -275,11 +275,11 @@
   When implementing proof methods, it is advisable to study existing
   implementations carefully and imitate the typical ``boiler plate''
   for context-sensitive parsing and further combinators to wrap-up
-  tactic expressions as methods.\footnote{Aliases or abbreviations of
+  tactic expressions as methods.\<^footnote>\<open>Aliases or abbreviations of
   the standard method combinators should be avoided.  Note that from
   Isabelle99 until Isabelle2009 the system did provide various odd
   combinations of method syntax wrappers that made applications more
-  complicated than necessary.}
+  complicated than necessary.\<close>
 \<close>
 
 text %mlref \<open>
diff -r 9c50eb3bff50 -r ddb3ac3fef45 src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Wed Nov 04 18:14:28 2015 +0100
+++ b/src/Doc/Implementation/Logic.thy	Wed Nov 04 18:32:47 2015 +0100
@@ -19,11 +19,11 @@
   Derivations are relative to a logical theory, which declares type
   constructors, constants, and axioms.  Theory declarations support
   schematic polymorphism, which is strictly speaking outside the
-  logic.\footnote{This is the deeper logical reason, why the theory
+  logic.\<^footnote>\<open>This is the deeper logical reason, why the theory
   context \<open>\<Theta>\<close> is separate from the proof context \<open>\<Gamma>\<close>
   of the core calculus: type constructors, term constants, and facts
   (proof constants) may involve arbitrary type schemes, but the type
-  of a locally fixed term parameter is also fixed!}
+  of a locally fixed term parameter is also fixed!\<close>
 \<close>
 
 
@@ -531,9 +531,9 @@
   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{This is the key difference to ``\<open>\<lambda>HOL\<close>'' in
+  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 for propositions and types.}
+  \<open>x : A\<close> are treated uniformly for propositions and types.\<close>
 
   \<^medskip>
   The axiomatization of a theory is implicitly closed by
diff -r 9c50eb3bff50 -r ddb3ac3fef45 src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Wed Nov 04 18:14:28 2015 +0100
+++ b/src/Doc/Implementation/ML.thy	Wed Nov 04 18:32:47 2015 +0100
@@ -23,11 +23,11 @@
   first-hand explanations should help to understand how proper
   Isabelle/ML is to be read and written, and to get access to the
   wealth of experience that is expressed in the source text and its
-  history of changes.\footnote{See
+  history of changes.\<^footnote>\<open>See
   @{url "http://isabelle.in.tum.de/repos/isabelle"} for the full
   Mercurial history.  There are symbolic tags to refer to official
   Isabelle releases, as opposed to arbitrary \<^emph>\<open>tip\<close> versions that
-  merely reflect snapshots that are never really up-to-date.}\<close>
+  merely reflect snapshots that are never really up-to-date.\<close>\<close>
 
 
 section \<open>Style and orthography\<close>
@@ -37,10 +37,10 @@
   to tell an informed reader what is really going on and how things
   really work.  This is a non-trivial aim, but it is supported by a
   certain style of writing Isabelle/ML that has emerged from long
-  years of system development.\footnote{See also the interesting style
+  years of system development.\<^footnote>\<open>See also the interesting style
   guide for OCaml
   @{url "http://caml.inria.fr/resources/doc/guides/guidelines.en.html"}
-  which shares many of our means and ends.}
+  which shares many of our means and ends.\<close>
 
   The main principle behind any coding style is \<^emph>\<open>consistency\<close>.
   For a single author of a small program this merely means ``choose
@@ -123,10 +123,10 @@
   For historical reasons, many capitalized names omit underscores,
   e.g.\ old-style @{ML_text FooBar} instead of @{ML_text Foo_Bar}.
   Genuine mixed-case names are \<^emph>\<open>not\<close> used, because clear division
-  of words is essential for readability.\footnote{Camel-case was
+  of words is essential for readability.\<^footnote>\<open>Camel-case was
   invented to workaround the lack of underscore in some early
   non-ASCII character sets.  Later it became habitual in some language
-  communities that are now strong in numbers.}
+  communities that are now strong in numbers.\<close>
 
   A single (capital) character does not count as ``word'' in this
   respect: some Isabelle/ML names are suffixed by extra markers like
@@ -279,10 +279,10 @@
 
 paragraph \<open>Line length\<close>
 text \<open>is limited to 80 characters according to ancient standards, but we allow
-  as much as 100 characters (not more).\footnote{Readability requires to keep
+  as much as 100 characters (not more).\<^footnote>\<open>Readability requires to keep
   the beginning of a line in view while watching its end. Modern wide-screen
   displays do not change the way how the human brain works. Sources also need
-  to be printable on plain paper with reasonable font-size.} The extra 20
+  to be printable on plain paper with reasonable font-size.\<close> The extra 20
   characters acknowledge the space requirements due to qualified library
   references in Isabelle/ML.\<close>
 
@@ -327,11 +327,11 @@
 \<close>
 
 paragraph \<open>Indentation\<close>
-text \<open>uses plain spaces, never hard tabulators.\footnote{Tabulators were
+text \<open>uses plain spaces, never hard tabulators.\<^footnote>\<open>Tabulators were
   invented to move the carriage of a type-writer to certain predefined
   positions. In software they could be used as a primitive run-length
   compression of consecutive spaces, but the precise result would depend on
-  non-standardized text editor configuration.}
+  non-standardized text editor configuration.\<close>
 
   Each level of nesting is indented by 2 spaces, sometimes 1, very
   rarely 4, never 8 or any other odd number.
@@ -562,10 +562,10 @@
   Removing the above ML declaration from the source text will remove any trace
   of this definition, as expected. The Isabelle/ML toplevel environment is
   managed in a \<^emph>\<open>stateless\<close> way: in contrast to the raw ML toplevel, there
-  are no global side-effects involved here.\footnote{Such a stateless
+  are no global side-effects involved here.\<^footnote>\<open>Such a stateless
   compilation environment is also a prerequisite for robust parallel
   compilation within independent nodes of the implicit theory development
-  graph.}
+  graph.\<close>
 
   \<^medskip>
   The next example shows how to embed ML into Isar proofs, using
@@ -739,9 +739,9 @@
   type \<open>\<tau>\<close> is represented by the iterated function space
   \<open>\<tau>\<^sub>1 \<rightarrow> \<dots> \<rightarrow> \<tau>\<^sub>n \<rightarrow> \<tau>\<close>.  This is isomorphic to the well-known
   encoding via tuples \<open>\<tau>\<^sub>1 \<times> \<dots> \<times> \<tau>\<^sub>n \<rightarrow> \<tau>\<close>, but the curried
-  version fits more smoothly into the basic calculus.\footnote{The
+  version fits more smoothly into the basic calculus.\<^footnote>\<open>The
   difference is even more significant in HOL, because the redundant
-  tuple structure needs to be accommodated extraneous proof steps.}
+  tuple structure needs to be accommodated extraneous proof steps.\<close>
 
   Currying gives some flexibility due to \<^emph>\<open>partial application\<close>.  A
   function \<open>f: \<tau>\<^sub>1 \<rightarrow> \<tau>\<^sub>2 \<rightarrow> \<tau>\<close> can be applied to \<open>x: \<tau>\<^sub>1\<close>
@@ -1282,9 +1282,9 @@
   \<^descr> @{ML "Symbol.explode"}~\<open>str\<close> produces a symbol list
   from the packed form.  This function supersedes @{ML
   "String.explode"} for virtually all purposes of manipulating text in
-  Isabelle!\footnote{The runtime overhead for exploded strings is
+  Isabelle!\<^footnote>\<open>The runtime overhead for exploded strings is
   mainly that of the list structure: individual symbols that happen to
-  be a singleton string do not require extra memory in Poly/ML.}
+  be a singleton string do not require extra memory in Poly/ML.\<close>
 
   \<^descr> @{ML "Symbol.is_letter"}, @{ML "Symbol.is_digit"}, @{ML
   "Symbol.is_quasi"}, @{ML "Symbol.is_blank"} classify standard
@@ -1396,8 +1396,8 @@
 
   \<^descr> Type @{ML_type int} represents regular mathematical integers, which
   are \<^emph>\<open>unbounded\<close>. Overflow is treated properly, but should never happen
-  in practice.\footnote{The size limit for integer bit patterns in memory is
-  64\,MB for 32-bit Poly/ML, and much higher for 64-bit systems.} This works
+  in practice.\<^footnote>\<open>The size limit for integer bit patterns in memory is
+  64\,MB for 32-bit Poly/ML, and much higher for 64-bit systems.\<close> This works
   uniformly for all supported ML platforms (Poly/ML and SML/NJ).
 
   Literal integers in ML text are forced to be of this one true
@@ -1614,13 +1614,13 @@
   sub-components with explicit communication, general asynchronous
   interaction etc.  Moreover, parallel evaluation is a prerequisite to
   make adequate use of the CPU resources that are available on
-  multi-core systems.\footnote{Multi-core computing does not mean that
+  multi-core systems.\<^footnote>\<open>Multi-core computing does not mean that
   there are ``spare cycles'' to be wasted.  It means that the
   continued 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"}.}
+  @{cite "Sutter:2005"}.\<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
@@ -1671,8 +1671,8 @@
 
   \<^item> Global references (or arrays), i.e.\ mutable memory cells that
   persist over several invocations of associated
-  operations.\footnote{This is independent of the visibility of such
-  mutable values in the toplevel scope.}
+  operations.\<^footnote>\<open>This is independent of the visibility of such
+  mutable values in the toplevel scope.\<close>
 
   \<^item> Global state of the running Isabelle/ML process, i.e.\ raw I/O
   channels, environment variables, current working directory.
diff -r 9c50eb3bff50 -r ddb3ac3fef45 src/Doc/Implementation/Syntax.thy
--- a/src/Doc/Implementation/Syntax.thy	Wed Nov 04 18:14:28 2015 +0100
+++ b/src/Doc/Implementation/Syntax.thy	Wed Nov 04 18:32:47 2015 +0100
@@ -20,9 +20,9 @@
   Moreover, type-inference in the style of Hindley-Milner @{cite hindleymilner}
   (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{Type-inference taken to the extreme can easily confuse
+  context.\<^footnote>\<open>Type-inference taken to the extreme can easily confuse
   users. Beginners often stumble over unexpectedly general types inferred by
-  the system.}
+  the system.\<close>
 
   \<^medskip>
   The main inner syntax operations are \<^emph>\<open>read\<close> for
diff -r 9c50eb3bff50 -r ddb3ac3fef45 src/Doc/Implementation/Tactic.thy
--- a/src/Doc/Implementation/Tactic.thy	Wed Nov 04 18:14:28 2015 +0100
+++ b/src/Doc/Implementation/Tactic.thy	Wed Nov 04 18:32:47 2015 +0100
@@ -18,10 +18,10 @@
   Isabelle/Pure represents a goal as a theorem stating that the
   subgoals imply the main goal: \<open>A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow>
   C\<close>.  The outermost goal structure is that of a Horn Clause: i.e.\
-  an iterated implication without any quantifiers\footnote{Recall that
+  an iterated implication without any quantifiers\<^footnote>\<open>Recall that
   outermost \<open>\<And>x. \<phi>[x]\<close> is always represented via schematic
   variables in the body: \<open>\<phi>[?x]\<close>.  These variables may get
-  instantiated during the course of reasoning.}.  For \<open>n = 0\<close>
+  instantiated during the course of reasoning.\<close>.  For \<open>n = 0\<close>
   a goal is called ``solved''.
 
   The structure of each subgoal \<open>A\<^sub>i\<close> is that of a
@@ -90,11 +90,11 @@
   \secref{sec:tactical-goals}) to a lazy sequence of potential
   successor states.  The underlying sequence implementation is lazy
   both in head and tail, and is purely functional in \<^emph>\<open>not\<close>
-  supporting memoing.\footnote{The lack of memoing and the strict
+  supporting memoing.\<^footnote>\<open>The lack of memoing and the strict
   nature of ML requires some care when working with low-level
   sequence operations, to avoid duplicate or premature evaluation of
   results.  It also means that modified runtime behavior, such as
-  timeout, is very hard to achieve for general tactics.}
+  timeout, is very hard to achieve for general tactics.\<close>
 
   An \<^emph>\<open>empty result sequence\<close> means that the tactic has failed: in
   a compound tactic expression other tactics might be tried instead,
@@ -319,12 +319,12 @@
   \<^descr> @{ML match_tac}, @{ML ematch_tac}, @{ML dmatch_tac}, and @{ML
   bimatch_tac} are similar to @{ML resolve_tac}, @{ML eresolve_tac},
   @{ML dresolve_tac}, and @{ML biresolve_tac}, respectively, but do
-  not instantiate schematic variables in the goal state.%
-\footnote{Strictly speaking, matching means to treat the unknowns in the goal
+  not instantiate schematic variables in the goal state.\<^footnote>\<open>Strictly speaking,
+  matching means to treat the unknowns in the goal
   state as constants, but these tactics merely discard unifiers that would
   update the goal state. In rare situations (where the conclusion and 
   goal state have flexible terms at the same position), the tactic
-  will fail even though an acceptable unifier exists.}
+  will fail even though an acceptable unifier exists.\<close>
   These tactics were written for a specific application within the classical reasoner.
 
   Flexible subgoals are not updated at will, but are left alone.
diff -r 9c50eb3bff50 -r ddb3ac3fef45 src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Wed Nov 04 18:14:28 2015 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy	Wed Nov 04 18:32:47 2015 +0100
@@ -327,9 +327,9 @@
 
   \<^descr> @{method simp_all} is similar to @{method simp}, but acts on
   all goals, working backwards from the last to the first one as usual
-  in Isabelle.\footnote{The order is irrelevant for goals without
+  in Isabelle.\<^footnote>\<open>The order is irrelevant for goals without
   schematic variables, so simplification might actually be performed
-  in parallel here.}
+  in parallel here.\<close>
 
   Chained facts are inserted into all subgoals, before the
   simplification process starts.  Further rule declarations are the
@@ -347,8 +347,8 @@
   normalization process, or simplifying assumptions themselves.
   Further options allow to fine-tune the behavior of the Simplifier
   in this respect, corresponding to a variety of ML tactics as
-  follows.\footnote{Unlike the corresponding Isar proof methods, the
-  ML tactics do not insist in changing the goal state.}
+  follows.\<^footnote>\<open>Unlike the corresponding Isar proof methods, the
+  ML tactics do not insist in changing the goal state.\<close>
 
   \begin{center}
   \small
@@ -1179,9 +1179,9 @@
   is easier to automate.
 
   A \<^bold>\<open>sequent\<close> has the form \<open>\<Gamma> \<turnstile> \<Delta>\<close>, where \<open>\<Gamma>\<close>
-  and \<open>\<Delta>\<close> are sets of formulae.\footnote{For first-order
+  and \<open>\<Delta>\<close> are sets of formulae.\<^footnote>\<open>For first-order
   logic, sequents can equivalently be made from lists or multisets of
-  formulae.} The sequent \<open>P\<^sub>1, \<dots>, P\<^sub>m \<turnstile> Q\<^sub>1, \<dots>, Q\<^sub>n\<close> is
+  formulae.\<close> The sequent \<open>P\<^sub>1, \<dots>, P\<^sub>m \<turnstile> Q\<^sub>1, \<dots>, Q\<^sub>n\<close> is
   \<^bold>\<open>valid\<close> if \<open>P\<^sub>1 \<and> \<dots> \<and> P\<^sub>m\<close> implies \<open>Q\<^sub>1 \<or> \<dots> \<or>
   Q\<^sub>n\<close>.  Thus \<open>P\<^sub>1, \<dots>, P\<^sub>m\<close> represent assumptions, each of which
   is true, while \<open>Q\<^sub>1, \<dots>, Q\<^sub>n\<close> represent alternative goals.  A
diff -r 9c50eb3bff50 -r ddb3ac3fef45 src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Wed Nov 04 18:14:28 2015 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Wed Nov 04 18:32:47 2015 +0100
@@ -277,8 +277,8 @@
   used internally in Isabelle/Pure.
 
   \<^item> \<^verbatim>\<open>xsymbols\<close>: enable proper mathematical symbols
-  instead of ASCII art.\footnote{This traditional mode name stems from
-  the ``X-Symbol'' package for classic Proof~General with XEmacs.}
+  instead of ASCII art.\<^footnote>\<open>This traditional mode name stems from
+  the ``X-Symbol'' package for classic Proof~General with XEmacs.\<close>
 
   \<^item> \<^verbatim>\<open>latex\<close>: additional mode that is active in {\LaTeX}
   document preparation of Isabelle theory sources; allows to provide
@@ -338,9 +338,9 @@
   grammar, where for each argument \<open>i\<close> the syntactic category
   is determined by \<open>\<tau>\<^sub>i\<close> (with priority \<open>p\<^sub>i\<close>), and the
   result category is determined from \<open>\<tau>\<close> (with priority \<open>p\<close>).  Priority specifications are optional, with default 0 for
-  arguments and 1000 for the result.\footnote{Omitting priorities is
+  arguments and 1000 for the result.\<^footnote>\<open>Omitting priorities is
   prone to syntactic ambiguities unless the delimiter tokens determine
-  fully bracketed notation, as in \<open>if _ then _ else _ fi\<close>.}
+  fully bracketed notation, as in \<open>if _ then _ else _ fi\<close>.\<close>
 
   Since \<open>\<tau>\<close> may be again a function type, the constant
   type scheme may have more argument positions than the mixfix
@@ -1213,10 +1213,10 @@
   side-conditions:
 
     \<^item> Rules must be left linear: \<open>lhs\<close> must not contain
-    repeated variables.\footnote{The deeper reason for this is that AST
+    repeated variables.\<^footnote>\<open>The deeper reason for this is that AST
     equality is not well-defined: different occurrences of the ``same''
     AST could be decorated differently by accidental type-constraints or
-    source position information, for example.}
+    source position information, for example.\<close>
 
     \<^item> Every variable in \<open>rhs\<close> must also occur in \<open>lhs\<close>.
 
diff -r 9c50eb3bff50 -r ddb3ac3fef45 src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Wed Nov 04 18:14:28 2015 +0100
+++ b/src/Doc/Isar_Ref/Proof.thy	Wed Nov 04 18:32:47 2015 +0100
@@ -530,8 +530,8 @@
 
   \<^medskip>
   The Isar calculation proof commands may be defined as
-  follows:\footnote{We suppress internal bookkeeping such as proper
-  handling of block-structure.}
+  follows:\<^footnote>\<open>We suppress internal bookkeeping such as proper
+  handling of block-structure.\<close>
 
   \begin{matharray}{rcl}
     @{command "also"}\<open>\<^sub>0\<close> & \equiv & @{command "note"}~\<open>calculation = this\<close> \\
@@ -718,9 +718,9 @@
   If the goal had been \<open>show\<close> (or \<open>thus\<close>), some
   pending sub-goal is solved as well by the rule resulting from the
   result \<^emph>\<open>exported\<close> into the enclosing goal context.  Thus \<open>qed\<close> may fail for two reasons: either \<open>m\<^sub>2\<close> fails, or the
-  resulting rule does not fit to any pending goal\footnote{This
+  resulting rule does not fit to any pending goal\<^footnote>\<open>This
   includes any additional ``strong'' assumptions as introduced by
-  @{command "assume"}.} of the enclosing context.  Debugging such a
+  @{command "assume"}.\<close> of the enclosing context.  Debugging such a
   situation might involve temporarily changing @{command "show"} into
   @{command "have"}, or weakening the local context by replacing
   occurrences of @{command "assume"} by @{command "presume"}.
diff -r 9c50eb3bff50 -r ddb3ac3fef45 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Wed Nov 04 18:14:28 2015 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Wed Nov 04 18:32:47 2015 +0100
@@ -39,9 +39,9 @@
   between ML and Scala, using asynchronous protocol commands.
 
   \<^descr>[jEdit] is a sophisticated text editor implemented in
-  Java.\footnote{@{url "http://www.jedit.org"}} It is easily extensible
+  Java.\<^footnote>\<open>@{url "http://www.jedit.org"}\<close> It is easily extensible
   by plugins written in languages that work on the JVM, e.g.\
-  Scala\footnote{@{url "http://www.scala-lang.org"}}.
+  Scala\<^footnote>\<open>@{url "http://www.scala-lang.org"}\<close>.
 
   \<^descr>[Isabelle/jEdit] is the main example application of the PIDE
   framework and the default user-interface for Isabelle. It targets
@@ -287,13 +287,13 @@
   default.
 
   \<^emph>\<open>GTK+\<close> also works under the side-condition that the overall GTK theme
-  is selected in a Swing-friendly way.\footnote{GTK support in Java/Swing was
+  is selected in a Swing-friendly way.\<^footnote>\<open>GTK support in Java/Swing was
   once marketed aggressively by Sun, but never quite finished. Today (2015) it
   is lagging behind further development of Swing and GTK. The graphics
   rendering performance can be worse than for other Swing look-and-feels.
   Nonetheless it has its uses for displays with very high resolution (such as
   ``4K'' or ``UHD'' models), because the rendering by the external library is
-  subject to global system settings for font scaling.}
+  subject to global system settings for font scaling.\<close>
 
   \<^descr>[Windows:] Regular \<^emph>\<open>Windows\<close> is used by default, but
   \<^emph>\<open>Windows Classic\<close> also works.
@@ -439,10 +439,10 @@
   Isabelle sources consist of \<^emph>\<open>symbols\<close> that extend plain ASCII to allow
   infinitely many mathematical symbols within the formal sources. This works
   without depending on particular encodings and varying Unicode
-  standards.\footnote{Raw Unicode characters within formal sources would
+  standards.\<^footnote>\<open>Raw Unicode characters within formal sources would
   compromise portability and reliability in the face of changing
   interpretation of special features of Unicode, such as Combining Characters
-  or Bi-directional Text.} See also @{cite "Wenzel:2011:CICM"}.
+  or Bi-directional Text.\<close> See also @{cite "Wenzel:2011:CICM"}.
 
   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
@@ -663,8 +663,8 @@
 
   The Java notation for files needs to be distinguished from the one of
   Isabelle, which uses POSIX notation with forward slashes on \<^emph>\<open>all\<close>
-  platforms.\footnote{Isabelle/ML on Windows uses Cygwin file-system access
-  and Unix-style path notation.} Moreover, environment variables from the
+  platforms.\<^footnote>\<open>Isabelle/ML on Windows uses Cygwin file-system access
+  and Unix-style path notation.\<close> Moreover, environment variables from the
   Isabelle process may be used freely, e.g.\ @{file
   "$ISABELLE_HOME/etc/symbols"} or @{file_unchecked "$POLYML_HOME/README"}.
   There are special shortcuts: @{file "~"} for @{file "$USER_HOME"} and @{file
@@ -926,9 +926,9 @@
   markup, while using secondary output windows only rarely.
 
   The main purpose of the output window is to ``debug'' unclear
-  situations by inspecting internal state of the prover.\footnote{In
+  situations by inspecting internal state of the prover.\<^footnote>\<open>In
   that sense, unstructured tactic scripts depend on continuous
-  debugging with internal state inspection.} Consequently, some
+  debugging with internal state inspection.\<close> Consequently, some
   special messages for \<^emph>\<open>tracing\<close> or \<^emph>\<open>proof state\<close> only
   appear here, and are not attached to the original source.
 
@@ -975,8 +975,8 @@
 
   \<^item> The \<^emph>\<open>Search\<close> field allows to highlight query output according to
   some regular expression, in the notation that is commonly used on the Java
-  platform.\footnote{@{url
-  "http://docs.oracle.com/javase/7/docs/api/java/util/regex/Pattern.html"}}
+  platform.\<^footnote>\<open>@{url
+  "http://docs.oracle.com/javase/7/docs/api/java/util/regex/Pattern.html"}\<close>
   This may serve as an additional visual filter of the result.
 
   \<^item> The \<^emph>\<open>Zoom\<close> box controls the font size of the output area.
diff -r 9c50eb3bff50 -r ddb3ac3fef45 src/Doc/System/Basics.thy
--- a/src/Doc/System/Basics.thy	Wed Nov 04 18:14:28 2015 +0100
+++ b/src/Doc/System/Basics.thy	Wed Nov 04 18:32:47 2015 +0100
@@ -141,9 +141,9 @@
   user home directory.  On Unix systems this is usually the same as
   @{setting HOME}, but on Windows it is the regular home directory of
   the user, not the one of within the Cygwin root
-  file-system.\footnote{Cygwin itself offers another choice whether
+  file-system.\<^footnote>\<open>Cygwin itself offers another choice whether
   its HOME should point to the @{file_unchecked "/home"} directory tree or the
-  Windows user home.}
+  Windows user home.\<close>
 
   \<^descr>[@{setting_def ISABELLE_HOME}\<open>\<^sup>*\<close>] is the location of the
   top-level Isabelle distribution directory. This is automatically
diff -r 9c50eb3bff50 -r ddb3ac3fef45 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Wed Nov 04 18:14:28 2015 +0100
+++ b/src/Doc/System/Sessions.thy	Wed Nov 04 18:32:47 2015 +0100
@@ -259,8 +259,8 @@
   related sources of theories and auxiliary files, and target heap
   images.  Accordingly, it runs instances of the prover process with
   optional document preparation.  Its command-line usage
-  is:\footnote{Isabelle/Scala provides the same functionality via
-  \<^verbatim>\<open>isabelle.Build.build\<close>.}
+  is:\<^footnote>\<open>Isabelle/Scala provides the same functionality via
+  \<^verbatim>\<open>isabelle.Build.build\<close>.\<close>
   @{verbatim [display]
 \<open>Usage: isabelle build [OPTIONS] [SESSIONS ...]