# 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>\This enables the user to write method expressions like \meth\<^sup>+\ without looping, while the trivial do-nothing case can be recovered - via \meth\<^sup>?\.} + via \meth\<^sup>?\.\ 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>\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.\ \ text %mlref \ 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>\This is the deeper logical reason, why the theory context \\\ is separate from the proof context \\\ 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!\ \ @@ -531,9 +531,9 @@ the simple syntactic types of Pure are always inhabitable. ``Assumptions'' \x :: \\ for type-membership are only present as long as some \x\<^sub>\\ occurs in the statement - body.\footnote{This is the key difference to ``\\HOL\'' in + body.\<^footnote>\This is the key difference to ``\\HOL\'' in the PTS framework @{cite "Barendregt-Geuvers:2001"}, where hypotheses - \x : A\ are treated uniformly for propositions and types.} + \x : A\ are treated uniformly for propositions and types.\ \<^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>\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>\tip\ versions that - merely reflect snapshots that are never really up-to-date.}\ + merely reflect snapshots that are never really up-to-date.\\ section \Style and orthography\ @@ -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>\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.\ The main principle behind any coding style is \<^emph>\consistency\. 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>\not\ used, because clear division - of words is essential for readability.\footnote{Camel-case was + of words is essential for readability.\<^footnote>\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.\ 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 \Line length\ text \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>\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.\ The extra 20 characters acknowledge the space requirements due to qualified library references in Isabelle/ML.\ @@ -327,11 +327,11 @@ \ paragraph \Indentation\ -text \uses plain spaces, never hard tabulators.\footnote{Tabulators were +text \uses plain spaces, never hard tabulators.\<^footnote>\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.\ 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>\stateless\ 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>\Such a stateless compilation environment is also a prerequisite for robust parallel compilation within independent nodes of the implicit theory development - graph.} + graph.\ \<^medskip> The next example shows how to embed ML into Isar proofs, using @@ -739,9 +739,9 @@ type \\\ is represented by the iterated function space \\\<^sub>1 \ \ \ \\<^sub>n \ \\. This is isomorphic to the well-known encoding via tuples \\\<^sub>1 \ \ \ \\<^sub>n \ \\, but the curried - version fits more smoothly into the basic calculus.\footnote{The + version fits more smoothly into the basic calculus.\<^footnote>\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.\ Currying gives some flexibility due to \<^emph>\partial application\. A function \f: \\<^sub>1 \ \\<^sub>2 \ \\ can be applied to \x: \\<^sub>1\ @@ -1282,9 +1282,9 @@ \<^descr> @{ML "Symbol.explode"}~\str\ 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>\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.\ \<^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>\unbounded\. 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>\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 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>\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"}.\ Isabelle/Isar exploits the inherent structure of theories and proofs to support \<^emph>\implicit parallelism\ 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>\This is independent of the visibility of such + mutable values in the toplevel scope.\ \<^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 \\x. B x\ concisely, when the type \'a\ is already clear from the - context.\footnote{Type-inference taken to the extreme can easily confuse + context.\<^footnote>\Type-inference taken to the extreme can easily confuse users. Beginners often stumble over unexpectedly general types inferred by - the system.} + the system.\ \<^medskip> The main inner syntax operations are \<^emph>\read\ 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: \A\<^sub>1 \ \ \ A\<^sub>n \ C\. 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>\Recall that outermost \\x. \[x]\ is always represented via schematic variables in the body: \\[?x]\. These variables may get - instantiated during the course of reasoning.}. For \n = 0\ + instantiated during the course of reasoning.\. For \n = 0\ a goal is called ``solved''. The structure of each subgoal \A\<^sub>i\ 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>\not\ - supporting memoing.\footnote{The lack of memoing and the strict + supporting memoing.\<^footnote>\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.\ An \<^emph>\empty result sequence\ 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>\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.\ 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>\The order is irrelevant for goals without schematic variables, so simplification might actually be performed - in parallel here.} + in parallel here.\ 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>\Unlike the corresponding Isar proof methods, the + ML tactics do not insist in changing the goal state.\ \begin{center} \small @@ -1179,9 +1179,9 @@ is easier to automate. A \<^bold>\sequent\ has the form \\ \ \\, where \\\ - and \\\ are sets of formulae.\footnote{For first-order + and \\\ are sets of formulae.\<^footnote>\For first-order logic, sequents can equivalently be made from lists or multisets of - formulae.} The sequent \P\<^sub>1, \, P\<^sub>m \ Q\<^sub>1, \, Q\<^sub>n\ is + formulae.\ The sequent \P\<^sub>1, \, P\<^sub>m \ Q\<^sub>1, \, Q\<^sub>n\ is \<^bold>\valid\ if \P\<^sub>1 \ \ \ P\<^sub>m\ implies \Q\<^sub>1 \ \ \ Q\<^sub>n\. Thus \P\<^sub>1, \, P\<^sub>m\ represent assumptions, each of which is true, while \Q\<^sub>1, \, Q\<^sub>n\ 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>\xsymbols\: 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>\This traditional mode name stems from + the ``X-Symbol'' package for classic Proof~General with XEmacs.\ \<^item> \<^verbatim>\latex\: 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 \i\ the syntactic category is determined by \\\<^sub>i\ (with priority \p\<^sub>i\), and the result category is determined from \\\ (with priority \p\). 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>\Omitting priorities is prone to syntactic ambiguities unless the delimiter tokens determine - fully bracketed notation, as in \if _ then _ else _ fi\.} + fully bracketed notation, as in \if _ then _ else _ fi\.\ Since \\\ 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: \lhs\ must not contain - repeated variables.\footnote{The deeper reason for this is that AST + repeated variables.\<^footnote>\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.\ \<^item> Every variable in \rhs\ must also occur in \lhs\. 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>\We suppress internal bookkeeping such as proper + handling of block-structure.\ \begin{matharray}{rcl} @{command "also"}\\<^sub>0\ & \equiv & @{command "note"}~\calculation = this\ \\ @@ -718,9 +718,9 @@ If the goal had been \show\ (or \thus\), some pending sub-goal is solved as well by the rule resulting from the result \<^emph>\exported\ into the enclosing goal context. Thus \qed\ may fail for two reasons: either \m\<^sub>2\ fails, or the - resulting rule does not fit to any pending goal\footnote{This + resulting rule does not fit to any pending goal\<^footnote>\This includes any additional ``strong'' assumptions as introduced by - @{command "assume"}.} of the enclosing context. Debugging such a + @{command "assume"}.\ 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>\@{url "http://www.jedit.org"}\ 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>\@{url "http://www.scala-lang.org"}\. \<^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>\GTK+\ 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>\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.\ \<^descr>[Windows:] Regular \<^emph>\Windows\ is used by default, but \<^emph>\Windows Classic\ also works. @@ -439,10 +439,10 @@ Isabelle sources consist of \<^emph>\symbols\ 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>\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.\ 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>\a\'' 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>\all\ - platforms.\footnote{Isabelle/ML on Windows uses Cygwin file-system access - and Unix-style path notation.} Moreover, environment variables from the + platforms.\<^footnote>\Isabelle/ML on Windows uses Cygwin file-system access + and Unix-style path notation.\ 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>\In that sense, unstructured tactic scripts depend on continuous - debugging with internal state inspection.} Consequently, some + debugging with internal state inspection.\ Consequently, some special messages for \<^emph>\tracing\ or \<^emph>\proof state\ only appear here, and are not attached to the original source. @@ -975,8 +975,8 @@ \<^item> The \<^emph>\Search\ 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>\@{url + "http://docs.oracle.com/javase/7/docs/api/java/util/regex/Pattern.html"}\ This may serve as an additional visual filter of the result. \<^item> The \<^emph>\Zoom\ 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>\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.\ \<^descr>[@{setting_def ISABELLE_HOME}\\<^sup>*\] 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>\isabelle.Build.build\.} + is:\<^footnote>\Isabelle/Scala provides the same functionality via + \<^verbatim>\isabelle.Build.build\.\ @{verbatim [display] \Usage: isabelle build [OPTIONS] [SESSIONS ...]