--- 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>
--- 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
--- 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.
--- 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
--- 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.
--- 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
--- 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>.
--- 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"}.
--- 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.
--- 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
--- 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 ...]