# HG changeset patch
# User wenzelm
# Date 1447195169 -3600
# Node ID b98b237969c0cfabe82f847cfab6c1f0436ba85b
# Parent  2f89f0b13e0890853e2f1fe87eb7f1e646b63fb3
tuned whitespace;

diff -r 2f89f0b13e08 -r b98b237969c0 src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Tue Nov 10 23:21:02 2015 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Tue Nov 10 23:39:29 2015 +0100
@@ -4,18 +4,20 @@
 
 chapter \<open>Document preparation \label{ch:document-prep}\<close>
 
-text \<open>Isabelle/Isar provides a simple document preparation system
-  based on {PDF-\LaTeX}, with support for hyperlinks and bookmarks
-  within that format.  This allows to produce papers, books, theses
-  etc.\ from Isabelle theory sources.
+text \<open>
+  Isabelle/Isar provides a simple document preparation system based on
+  {PDF-\LaTeX}, with support for hyperlinks and bookmarks within that format.
+  This allows to produce papers, books, theses etc.\ from Isabelle theory
+  sources.
 
-  {\LaTeX} output is generated while processing a \<^emph>\<open>session\<close> in
-  batch mode, as explained in the \<^emph>\<open>The Isabelle System Manual\<close>
-  @{cite "isabelle-system"}.  The main Isabelle tools to get started with
-  document preparation are @{tool_ref mkroot} and @{tool_ref build}.
+  {\LaTeX} output is generated while processing a \<^emph>\<open>session\<close> in batch mode, as
+  explained in the \<^emph>\<open>The Isabelle System Manual\<close> @{cite "isabelle-system"}.
+  The main Isabelle tools to get started with document preparation are
+  @{tool_ref mkroot} and @{tool_ref build}.
 
-  The classic Isabelle/HOL tutorial @{cite "isabelle-hol-book"} also
-  explains some aspects of theory presentation.\<close>
+  The classic Isabelle/HOL tutorial @{cite "isabelle-hol-book"} also explains
+  some aspects of theory presentation.
+\<close>
 
 
 section \<open>Markup commands \label{sec:markup}\<close>
@@ -33,16 +35,15 @@
     @{command_def "text_raw"} & : & \<open>any \<rightarrow> any\<close> \\
   \end{matharray}
 
-  Markup commands provide a structured way to insert text into the
-  document generated from a theory.  Each markup command takes a
-  single @{syntax text} argument, which is passed as argument to a
-  corresponding {\LaTeX} macro.  The default macros provided by
-  @{file "~~/lib/texinputs/isabelle.sty"} can be redefined according
-  to the needs of the underlying document and {\LaTeX} styles.
+  Markup commands provide a structured way to insert text into the document
+  generated from a theory. Each markup command takes a single @{syntax text}
+  argument, which is passed as argument to a corresponding {\LaTeX} macro. The
+  default macros provided by @{file "~~/lib/texinputs/isabelle.sty"} can be
+  redefined according to the needs of the underlying document and {\LaTeX}
+  styles.
 
-  Note that formal comments (\secref{sec:comments}) are similar to
-  markup commands, but have a different status within Isabelle/Isar
-  syntax.
+  Note that formal comments (\secref{sec:comments}) are similar to markup
+  commands, but have a different status within Isabelle/Isar syntax.
 
   @{rail \<open>
     (@@{command chapter} | @@{command section} | @@{command subsection} |
@@ -50,28 +51,27 @@
       @@{command text} | @@{command txt} | @@{command text_raw}) @{syntax text}
   \<close>}
 
-  \<^descr> @{command chapter}, @{command section}, @{command subsection} etc.\ mark
-  section headings within the theory source. This works in any context, even
-  before the initial @{command theory} command. The corresponding {\LaTeX}
-  macros are \<^verbatim>\<open>\isamarkupchapter\<close>, \<^verbatim>\<open>\isamarkupsection\<close>, \<^verbatim>\<open>\isamarkupsubsection\<close> etc.\
+    \<^descr> @{command chapter}, @{command section}, @{command subsection} etc.\ mark
+    section headings within the theory source. This works in any context, even
+    before the initial @{command theory} command. The corresponding {\LaTeX}
+    macros are \<^verbatim>\<open>\isamarkupchapter\<close>, \<^verbatim>\<open>\isamarkupsection\<close>,
+    \<^verbatim>\<open>\isamarkupsubsection\<close> etc.\
 
-  \<^descr> @{command text} and @{command txt} specify paragraphs of plain text.
-  This corresponds to a {\LaTeX} environment \<^verbatim>\<open>\begin{isamarkuptext}\<close> \<open>\<dots>\<close>
-  \<^verbatim>\<open>\end{isamarkuptext}\<close> etc.
+    \<^descr> @{command text} and @{command txt} specify paragraphs of plain text.
+    This corresponds to a {\LaTeX} environment \<^verbatim>\<open>\begin{isamarkuptext}\<close> \<open>\<dots>\<close>
+    \<^verbatim>\<open>\end{isamarkuptext}\<close> etc.
 
-  \<^descr> @{command text_raw} is similar to @{command text}, but without
-  any surrounding markup environment. This allows to inject arbitrary
-  {\LaTeX} source into the generated document.
-
+    \<^descr> @{command text_raw} is similar to @{command text}, but without any
+    surrounding markup environment. This allows to inject arbitrary {\LaTeX}
+    source into the generated document.
 
   All text passed to any of the above markup commands may refer to formal
-  entities via \<^emph>\<open>document antiquotations\<close>, see also \secref{sec:antiq}.
-  These are interpreted in the present theory or proof context.
+  entities via \<^emph>\<open>document antiquotations\<close>, see also \secref{sec:antiq}. These
+  are interpreted in the present theory or proof context.
 
   \<^medskip>
-  The proof markup commands closely resemble those for theory
-  specifications, but have a different formal status and produce
-  different {\LaTeX} macros.
+  The proof markup commands closely resemble those for theory specifications,
+  but have a different formal status and produce different {\LaTeX} macros.
 \<close>
 
 
@@ -309,117 +309,110 @@
 
 subsection \<open>Styled antiquotations\<close>
 
-text \<open>The antiquotations \<open>thm\<close>, \<open>prop\<close> and \<open>term\<close> admit an extra \<^emph>\<open>style\<close> specification to modify the
-  printed result.  A style is specified by a name with a possibly
-  empty number of arguments;  multiple styles can be sequenced with
-  commas.  The following standard styles are available:
+text \<open>
+  The antiquotations \<open>thm\<close>, \<open>prop\<close> and \<open>term\<close> admit an extra \<^emph>\<open>style\<close>
+  specification to modify the printed result. A style is specified by a name
+  with a possibly empty number of arguments; multiple styles can be sequenced
+  with commas. The following standard styles are available:
 
-  \<^descr> \<open>lhs\<close> extracts the first argument of any application
-  form with at least two arguments --- typically meta-level or
-  object-level equality, or any other binary relation.
+  \<^descr> \<open>lhs\<close> extracts the first argument of any application form with at least
+  two arguments --- typically meta-level or object-level equality, or any
+  other binary relation.
   
-  \<^descr> \<open>rhs\<close> is like \<open>lhs\<close>, but extracts the second
-  argument.
+  \<^descr> \<open>rhs\<close> is like \<open>lhs\<close>, but extracts the second argument.
   
-  \<^descr> \<open>concl\<close> extracts the conclusion \<open>C\<close> from a rule
-  in Horn-clause normal form \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C\<close>.
+  \<^descr> \<open>concl\<close> extracts the conclusion \<open>C\<close> from a rule in Horn-clause normal form
+  \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C\<close>.
   
-  \<^descr> \<open>prem\<close> \<open>n\<close> extract premise number
-  \<open>n\<close> from from a rule in Horn-clause
-  normal form \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C\<close>
+  \<^descr> \<open>prem\<close> \<open>n\<close> extract premise number \<open>n\<close> from from a rule in Horn-clause
+  normal form \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C\<close>.
 \<close>
 
 
 subsection \<open>General options\<close>
 
-text \<open>The following options are available to tune the printed output
-  of antiquotations.  Note that many of these coincide with system and
+text \<open>
+  The following options are available to tune the printed output of
+  antiquotations. Note that many of these coincide with system and
   configuration options of the same names.
 
-  \<^descr> @{antiquotation_option_def show_types}~\<open>= bool\<close> and
-  @{antiquotation_option_def show_sorts}~\<open>= bool\<close> control
-  printing of explicit type and sort constraints.
+    \<^descr> @{antiquotation_option_def show_types}~\<open>= bool\<close> and
+    @{antiquotation_option_def show_sorts}~\<open>= bool\<close> control printing of
+    explicit type and sort constraints.
 
-  \<^descr> @{antiquotation_option_def show_structs}~\<open>= bool\<close>
-  controls printing of implicit structures.
+    \<^descr> @{antiquotation_option_def show_structs}~\<open>= bool\<close> controls printing of
+    implicit structures.
 
-  \<^descr> @{antiquotation_option_def show_abbrevs}~\<open>= bool\<close>
-  controls folding of abbreviations.
+    \<^descr> @{antiquotation_option_def show_abbrevs}~\<open>= bool\<close> controls folding of
+    abbreviations.
 
-  \<^descr> @{antiquotation_option_def names_long}~\<open>= bool\<close> forces
-  names of types and constants etc.\ to be printed in their fully
-  qualified internal form.
+    \<^descr> @{antiquotation_option_def names_long}~\<open>= bool\<close> forces names of types
+    and constants etc.\ to be printed in their fully qualified internal form.
 
-  \<^descr> @{antiquotation_option_def names_short}~\<open>= bool\<close>
-  forces names of types and constants etc.\ to be printed unqualified.
-  Note that internalizing the output again in the current context may
-  well yield a different result.
+    \<^descr> @{antiquotation_option_def names_short}~\<open>= bool\<close> forces names of types
+    and constants etc.\ to be printed unqualified. Note that internalizing the
+    output again in the current context may well yield a different result.
 
-  \<^descr> @{antiquotation_option_def names_unique}~\<open>= bool\<close>
-  determines whether the printed version of qualified names should be
-  made sufficiently long to avoid overlap with names declared further
-  back.  Set to \<open>false\<close> for more concise output.
+    \<^descr> @{antiquotation_option_def names_unique}~\<open>= bool\<close> determines whether the
+    printed version of qualified names should be made sufficiently long to
+    avoid overlap with names declared further back. Set to \<open>false\<close> for more
+    concise output.
 
-  \<^descr> @{antiquotation_option_def eta_contract}~\<open>= bool\<close>
-  prints terms in \<open>\<eta>\<close>-contracted form.
+    \<^descr> @{antiquotation_option_def eta_contract}~\<open>= bool\<close> prints terms in
+    \<open>\<eta>\<close>-contracted form.
 
-  \<^descr> @{antiquotation_option_def display}~\<open>= bool\<close> indicates
-  if the text is to be output as multi-line ``display material'',
-  rather than a small piece of text without line breaks (which is the
-  default).
+    \<^descr> @{antiquotation_option_def display}~\<open>= bool\<close> indicates if the text is to
+    be output as multi-line ``display material'', rather than a small piece of
+    text without line breaks (which is the default).
 
-  In this mode the embedded entities are printed in the same style as
-  the main theory text.
+    In this mode the embedded entities are printed in the same style as the
+    main theory text.
 
-  \<^descr> @{antiquotation_option_def break}~\<open>= bool\<close> controls
-  line breaks in non-display material.
+    \<^descr> @{antiquotation_option_def break}~\<open>= bool\<close> controls line breaks in
+    non-display material.
 
-  \<^descr> @{antiquotation_option_def quotes}~\<open>= bool\<close> indicates
-  if the output should be enclosed in double quotes.
-
-  \<^descr> @{antiquotation_option_def mode}~\<open>= name\<close> adds \<open>name\<close> to the print mode to be used for presentation.  Note that the
-  standard setup for {\LaTeX} output is already present by default,
-  including the modes \<open>latex\<close> and \<open>xsymbols\<close>.
+    \<^descr> @{antiquotation_option_def quotes}~\<open>= bool\<close> indicates if the output
+    should be enclosed in double quotes.
 
-  \<^descr> @{antiquotation_option_def margin}~\<open>= nat\<close> and
-  @{antiquotation_option_def indent}~\<open>= nat\<close> change the margin
-  or indentation for pretty printing of display material.
+    \<^descr> @{antiquotation_option_def mode}~\<open>= name\<close> adds \<open>name\<close> to the print mode
+    to be used for presentation. Note that the standard setup for {\LaTeX}
+    output is already present by default, including the modes \<open>latex\<close> and
+    \<open>xsymbols\<close>.
 
-  \<^descr> @{antiquotation_option_def goals_limit}~\<open>= nat\<close>
-  determines the maximum number of subgoals to be printed (for goal-based
-  antiquotation).
+    \<^descr> @{antiquotation_option_def margin}~\<open>= nat\<close> and
+    @{antiquotation_option_def indent}~\<open>= nat\<close> change the margin or
+    indentation for pretty printing of display material.
+
+    \<^descr> @{antiquotation_option_def goals_limit}~\<open>= nat\<close> determines the maximum
+    number of subgoals to be printed (for goal-based antiquotation).
 
-  \<^descr> @{antiquotation_option_def source}~\<open>= bool\<close> prints the
-  original source text of the antiquotation arguments, rather than its
-  internal representation.  Note that formal checking of
-  @{antiquotation "thm"}, @{antiquotation "term"}, etc. is still
-  enabled; use the @{antiquotation "text"} antiquotation for unchecked
-  output.
+    \<^descr> @{antiquotation_option_def source}~\<open>= bool\<close> prints the original source
+    text of the antiquotation arguments, rather than its internal
+    representation. Note that formal checking of @{antiquotation "thm"},
+    @{antiquotation "term"}, etc. is still enabled; use the @{antiquotation
+    "text"} antiquotation for unchecked output.
 
-  Regular \<open>term\<close> and \<open>typ\<close> antiquotations with \<open>source = false\<close> involve a full round-trip from the original source
-  to an internalized logical entity back to a source form, according
-  to the syntax of the current context.  Thus the printed output is
-  not under direct control of the author, it may even fluctuate a bit
-  as the underlying theory is changed later on.
+    Regular \<open>term\<close> and \<open>typ\<close> antiquotations with \<open>source = false\<close> involve a
+    full round-trip from the original source to an internalized logical entity
+    back to a source form, according to the syntax of the current context.
+    Thus the printed output is not under direct control of the author, it may
+    even fluctuate a bit as the underlying theory is changed later on.
 
-  In contrast, @{antiquotation_option source}~\<open>= true\<close>
-  admits direct printing of the given source text, with the desirable
-  well-formedness check in the background, but without modification of
-  the printed text.
+    In contrast, @{antiquotation_option source}~\<open>= true\<close> admits direct
+    printing of the given source text, with the desirable well-formedness
+    check in the background, but without modification of the printed text.
 
-
-  For Boolean flags, ``\<open>name = true\<close>'' may be abbreviated as
-  ``\<open>name\<close>''.  All of the above flags are disabled by default,
-  unless changed specifically for a logic session in the corresponding
-  \<^verbatim>\<open>ROOT\<close> file.
+  For Boolean flags, ``\<open>name = true\<close>'' may be abbreviated as ``\<open>name\<close>''. All
+  of the above flags are disabled by default, unless changed specifically for
+  a logic session in the corresponding \<^verbatim>\<open>ROOT\<close> file.
 \<close>
 
 
 section \<open>Markup via command tags \label{sec:tags}\<close>
 
-text \<open>Each Isabelle/Isar command may be decorated by additional
-  presentation tags, to indicate some modification in the way it is
-  printed in the document.
+text \<open>
+  Each Isabelle/Isar command may be decorated by additional presentation tags,
+  to indicate some modification in the way it is printed in the document.
 
   @{rail \<open>
     @{syntax_def tags}: ( tag * )
@@ -427,8 +420,8 @@
     tag: '%' (@{syntax ident} | @{syntax string})
   \<close>}
 
-  Some tags are pre-declared for certain classes of commands, serving
-  as default markup if no tags are given in the text:
+  Some tags are pre-declared for certain classes of commands, serving as
+  default markup if no tags are given in the text:
 
   \<^medskip>
   \begin{tabular}{ll}
@@ -438,34 +431,29 @@
   \end{tabular}
   \<^medskip>
 
-  The Isabelle document preparation system
-  @{cite "isabelle-system"} allows tagged command regions to be presented
-  specifically, e.g.\ to fold proof texts, or drop parts of the text
-  completely.
+  The Isabelle document preparation system @{cite "isabelle-system"} allows
+  tagged command regions to be presented specifically, e.g.\ to fold proof
+  texts, or drop parts of the text completely.
 
-  For example ``@{command "by"}~\<open>%invisible auto\<close>'' causes
-  that piece of proof to be treated as \<open>invisible\<close> instead of
-  \<open>proof\<close> (the default), which may be shown or hidden
-  depending on the document setup.  In contrast, ``@{command
-  "by"}~\<open>%visible auto\<close>'' forces this text to be shown
-  invariably.
+  For example ``@{command "by"}~\<open>%invisible auto\<close>'' causes that piece of proof
+  to be treated as \<open>invisible\<close> instead of \<open>proof\<close> (the default), which may be
+  shown or hidden depending on the document setup. In contrast, ``@{command
+  "by"}~\<open>%visible auto\<close>'' forces this text to be shown invariably.
 
-  Explicit tag specifications within a proof apply to all subsequent
-  commands of the same level of nesting.  For example, ``@{command
-  "proof"}~\<open>%visible \<dots>\<close>~@{command "qed"}'' forces the whole
-  sub-proof to be typeset as \<open>visible\<close> (unless some of its parts
-  are tagged differently).
+  Explicit tag specifications within a proof apply to all subsequent commands
+  of the same level of nesting. For example, ``@{command "proof"}~\<open>%visible
+  \<dots>\<close>~@{command "qed"}'' forces the whole sub-proof to be typeset as \<open>visible\<close>
+  (unless some of its parts are tagged differently).
 
   \<^medskip>
-  Command tags merely produce certain markup environments for
-  type-setting.  The meaning of these is determined by {\LaTeX}
-  macros, as defined in @{file "~~/lib/texinputs/isabelle.sty"} or
-  by the document author.  The Isabelle document preparation tools
-  also provide some high-level options to specify the meaning of
-  arbitrary tags to ``keep'', ``drop'', or ``fold'' the corresponding
-  parts of the text.  Logic sessions may also specify ``document
-  versions'', where given tags are interpreted in some particular way.
-  Again see @{cite "isabelle-system"} for further details.
+  Command tags merely produce certain markup environments for type-setting.
+  The meaning of these is determined by {\LaTeX} macros, as defined in @{file
+  "~~/lib/texinputs/isabelle.sty"} or by the document author. The Isabelle
+  document preparation tools also provide some high-level options to specify
+  the meaning of arbitrary tags to ``keep'', ``drop'', or ``fold'' the
+  corresponding parts of the text. Logic sessions may also specify ``document
+  versions'', where given tags are interpreted in some particular way. Again
+  see @{cite "isabelle-system"} for further details.
 \<close>
 
 
@@ -480,14 +468,13 @@
     'rail' @{syntax text}
   \<close>}
 
-  The @{antiquotation rail} antiquotation allows to include syntax
-  diagrams into Isabelle documents.  {\LaTeX} requires the style file
-  @{file "~~/lib/texinputs/railsetup.sty"}, which can be used via
+  The @{antiquotation rail} antiquotation allows to include syntax diagrams
+  into Isabelle documents. {\LaTeX} requires the style file @{file
+  "~~/lib/texinputs/railsetup.sty"}, which can be used via
   \<^verbatim>\<open>\usepackage{railsetup}\<close> in \<^verbatim>\<open>root.tex\<close>, for example.
 
-  The rail specification language is quoted here as Isabelle @{syntax
-  string} or text @{syntax "cartouche"}; it has its own grammar given
-  below.
+  The rail specification language is quoted here as Isabelle @{syntax string}
+  or text @{syntax "cartouche"}; it has its own grammar given below.
 
   \begingroup
   \def\isasymnewline{\isatt{\isacharbackslash\isacharless newline\isachargreater}}
@@ -506,15 +493,14 @@
   \<close>}
   \endgroup
 
-  The lexical syntax of \<open>identifier\<close> coincides with that of
-  @{syntax ident} in regular Isabelle syntax, but \<open>string\<close> uses
-  single quotes instead of double quotes of the standard @{syntax
-  string} category.
+  The lexical syntax of \<open>identifier\<close> coincides with that of @{syntax ident} in
+  regular Isabelle syntax, but \<open>string\<close> uses single quotes instead of double
+  quotes of the standard @{syntax string} category.
 
-  Each \<open>rule\<close> defines a formal language (with optional name),
-  using a notation that is similar to EBNF or regular expressions with
-  recursion.  The meaning and visual appearance of these rail language
-  elements is illustrated by the following representative examples.
+  Each \<open>rule\<close> defines a formal language (with optional name), using a notation
+  that is similar to EBNF or regular expressions with recursion. The meaning
+  and visual appearance of these rail language elements is illustrated by the
+  following representative examples.
 
   \<^item> Empty \<^verbatim>\<open>()\<close>
 
@@ -585,10 +571,9 @@
     @@{command display_drafts} (@{syntax name} +)
   \<close>}
 
-  \<^descr> @{command "display_drafts"}~\<open>paths\<close> performs simple output of a
-  given list of raw source files. Only those symbols that do not require
-  additional {\LaTeX} packages are displayed properly, everything else is left
-  verbatim.
+  \<^descr> @{command "display_drafts"}~\<open>paths\<close> performs simple output of a given list
+  of raw source files. Only those symbols that do not require additional
+  {\LaTeX} packages are displayed properly, everything else is left verbatim.
 \<close>
 
 end