1.1 --- a/doc-src/TutorialI/Documents/Documents.thy Tue Jan 15 10:24:20 2002 +0100
1.2 +++ b/doc-src/TutorialI/Documents/Documents.thy Tue Jan 15 13:14:39 2002 +0100
1.3 @@ -5,18 +5,19 @@
1.4 section {* Concrete Syntax \label{sec:concrete-syntax} *}
1.5
1.6 text {*
1.7 - The core concept of Isabelle's elaborate infrastructure for concrete
1.8 - syntax is that of general \bfindex{mixfix annotations}. Associated
1.9 + The core concept of Isabelle's framework for concrete
1.10 + syntax is that of \bfindex{mixfix annotations}. Associated
1.11 with any kind of constant declaration, mixfixes affect both the
1.12 grammar productions for the parser and output templates for the
1.13 pretty printer.
1.14
1.15 In full generality, parser and pretty printer configuration is a
1.16 - rather subtle affair, see \cite{isabelle-ref} for details. Syntax
1.17 - specifications given by end-users need to interact properly with the
1.18 - existing setup of Isabelle/Pure and Isabelle/HOL. It is
1.19 - particularly important to get the precedence of new syntactic
1.20 - constructs right, avoiding ambiguities with existing elements.
1.21 + subtle affair \cite{isabelle-ref}. Your syntax
1.22 + specifications need to interact properly with the
1.23 + existing setup of Isabelle/Pure and Isabelle/HOL\@.
1.24 + To avoid creating ambiguities with existing elements, it is
1.25 + particularly important to give new syntactic
1.26 + constructs the right precedence.
1.27
1.28 \medskip Subsequently we introduce a few simple syntax declaration
1.29 forms that already cover many common situations fairly well.
1.30 @@ -26,18 +27,17 @@
1.31 subsection {* Infix Annotations *}
1.32
1.33 text {*
1.34 - Syntax annotations may be included wherever constants are declared
1.35 - directly or indirectly, including \isacommand{consts},
1.36 - \isacommand{constdefs}, or \isacommand{datatype} (for the
1.37 - constructor operations). Type-constructors may be annotated as
1.38 + Syntax annotations may be included wherever constants are declared,
1.39 + such as \isacommand{consts} and
1.40 + \isacommand{constdefs} --- and also \isacommand{datatype}, which
1.41 + declares constructor operations. Type-constructors may be annotated as
1.42 well, although this is less frequently encountered in practice (the
1.43 infix type @{text "\<times>"} comes to mind).
1.44
1.45 Infix declarations\index{infix annotations} provide a useful special
1.46 - case of mixfixes, where users need not care about the full details
1.47 - of priorities, nesting, spacing, etc. The following example of the
1.48 + case of mixfixes. The following example of the
1.49 exclusive-or operation on boolean values illustrates typical infix
1.50 - declarations arising in practice.
1.51 + declarations.
1.52 *}
1.53
1.54 constdefs
1.55 @@ -47,16 +47,16 @@
1.56 text {*
1.57 \noindent Now @{text "xor A B"} and @{text "A [+] B"} refer to the
1.58 same expression internally. Any curried function with at least two
1.59 - arguments may be associated with infix syntax. For partial
1.60 - applications with less than two operands there is a special notation
1.61 - with \isa{op} prefix: @{text xor} without arguments is represented
1.62 - as @{text "op [+]"}; together with plain prefix application this
1.63 + arguments may be given infix syntax. For partial
1.64 + applications with fewer than two operands, there is a notation
1.65 + using the prefix~\isa{op}. For instance, @{text xor} without arguments is represented
1.66 + as @{text "op [+]"}; together with ordinary function application, this
1.67 turns @{text "xor A"} into @{text "op [+] A"}.
1.68
1.69 \medskip The keyword \isakeyword{infixl} seen above specifies an
1.70 infix operator that is nested to the \emph{left}: in iterated
1.71 applications the more complex expression appears on the left-hand
1.72 - side, @{term "A [+] B [+] C"} stands for @{text "(A [+] B) [+] C"}.
1.73 + side, and @{term "A [+] B [+] C"} stands for @{text "(A [+] B) [+] C"}.
1.74 Similarly, \isakeyword{infixr} specifies nesting to the
1.75 \emph{right}, reading @{term "A [+] B [+] C"} as @{text "A [+] (B
1.76 [+] C)"}. In contrast, a \emph{non-oriented} declaration via
1.77 @@ -65,21 +65,19 @@
1.78
1.79 The string @{text [source] "[+]"} in our annotation refers to the
1.80 concrete syntax to represent the operator (a literal token), while
1.81 - the number @{text 60} determines the precedence of the construct
1.82 - (i.e.\ the syntactic priorities of the arguments and result). As it
1.83 - happens, Isabelle/HOL already uses up many popular combinations of
1.84 + the number @{text 60} determines the precedence of the construct:
1.85 + the syntactic priorities of the arguments and result.
1.86 + Isabelle/HOL already uses up many popular combinations of
1.87 ASCII symbols for its own use, including both @{text "+"} and @{text
1.88 - "++"}. As a rule of thumb, more awkward character combinations are
1.89 - more likely to be still available for user extensions, just as our
1.90 - present @{text "[+]"}.
1.91 + "++"}. Longer character combinations are
1.92 + more likely to be still available for user extensions, such as our~@{text "[+]"}.
1.93
1.94 - Operator precedence also needs some special considerations. The
1.95 - admissible range is 0--1000. Very low or high priorities are
1.96 - basically reserved for the meta-logic. Syntax of Isabelle/HOL
1.97 + Operator precedences have a range of 0--1000. Very low or high priorities are
1.98 + reserved for the meta-logic. HOL syntax
1.99 mainly uses the range of 10--100: the equality infix @{text "="} is
1.100 - centered at 50, logical connectives (like @{text "\<or>"} and @{text
1.101 - "\<and>"}) are below 50, and algebraic ones (like @{text "+"} and @{text
1.102 - "*"}) above 50. User syntax should strive to coexist with common
1.103 + centered at 50; logical connectives (like @{text "\<or>"} and @{text
1.104 + "\<and>"}) are below 50; algebraic ones (like @{text "+"} and @{text
1.105 + "*"}) are above 50. User syntax should strive to coexist with common
1.106 HOL forms, or use the mostly unused range 100--900.
1.107
1.108 *}
1.109 @@ -88,8 +86,8 @@
1.110 subsection {* Mathematical Symbols \label{sec:syntax-symbols} *}
1.111
1.112 text {*
1.113 - Concrete syntax based on plain ASCII characters has its inherent
1.114 - limitations. Rich mathematical notation demands a larger repertoire
1.115 + Concrete syntax based on ASCII characters has inherent
1.116 + limitations. Mathematical notation demands a larger repertoire
1.117 of glyphs. Several standards of extended character sets have been
1.118 proposed over decades, but none has become universally available so
1.119 far. Isabelle supports a generic notion of \bfindex{symbols} as the
1.120 @@ -112,21 +110,20 @@
1.121 interpretation is left to further front-end tools. For example,
1.122 both the user-interface of Proof~General + X-Symbol and the Isabelle
1.123 document processor (see \S\ref{sec:document-preparation}) display
1.124 - the \verb,\,\verb,<forall>, symbol as @{text \<forall>}.
1.125 + the \verb,\,\verb,<forall>, symbol as~@{text \<forall>}.
1.126
1.127 A list of standard Isabelle symbols is given in
1.128 - \cite[appendix~A]{isabelle-sys}. Users may introduce their own
1.129 + \cite[appendix~A]{isabelle-sys}. You may introduce their own
1.130 interpretation of further symbols by configuring the appropriate
1.131 front-end tool accordingly, e.g.\ by defining certain {\LaTeX}
1.132 macros (see also \S\ref{sec:doc-prep-symbols}). There are also a
1.133 few predefined control symbols, such as \verb,\,\verb,<^sub>, and
1.134 \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent
1.135 - (printable) symbol, respectively. For example, \verb,A\<^sup>\<star>, is
1.136 + printable symbol, respectively. For example, \verb,A\<^sup>\<star>, is
1.137 output as @{text "A\<^sup>\<star>"}.
1.138
1.139 - \medskip The following version of our @{text xor} definition uses a
1.140 - standard Isabelle symbol to achieve typographically more pleasing
1.141 - output than before.
1.142 + \medskip Replacing our definition of @{text xor} by the following
1.143 + specifies a Isabelle symbol for the new operator:
1.144 *}
1.145
1.146 (*<*)
1.147 @@ -143,12 +140,12 @@
1.148 text {*
1.149 \noindent The X-Symbol package within Proof~General provides several
1.150 input methods to enter @{text \<oplus>} in the text. If all fails one may
1.151 - just type a named entity \verb,\,\verb,<oplus>, by hand; the display
1.152 - will be adapted immediately after continuing input.
1.153 + just type a named entity \verb,\,\verb,<oplus>, by hand; the
1.154 + corresponding symbol will immediately be displayed.
1.155
1.156 - \medskip A slightly more refined scheme of providing alternative
1.157 - syntax forms uses the \bfindex{print mode} concept of Isabelle (see
1.158 - also \cite{isabelle-ref}). By convention, the mode of
1.159 + \medskip More flexible is to provide alternative
1.160 + syntax forms through the \bfindex{print mode} concept~\cite{isabelle-ref}.
1.161 + By convention, the mode of
1.162 ``$xsymbols$'' is enabled whenever Proof~General's X-Symbol mode or
1.163 {\LaTeX} output is active. Now consider the following hybrid
1.164 declaration of @{text xor}:
1.165 @@ -179,8 +176,8 @@
1.166 \medskip We may now write @{text "A [+] B"} or @{text "A \<oplus> B"} in
1.167 input, while output uses the nicer syntax of $xsymbols$, provided
1.168 that print mode is active. Such an arrangement is particularly
1.169 - useful for interactive development, where users may type plain ASCII
1.170 - text, but gain improved visual feedback from the system.
1.171 + useful for interactive development, where users may type ASCII
1.172 + text and see mathematical symbols displayed during proofs.
1.173 *}
1.174
1.175
1.176 @@ -188,7 +185,7 @@
1.177
1.178 text {*
1.179 Prefix syntax annotations\index{prefix annotation} are another
1.180 - degenerate form of mixfixes \cite{isabelle-ref}, without any
1.181 + form of mixfixes \cite{isabelle-ref}, without any
1.182 template arguments or priorities --- just some bits of literal
1.183 syntax. The following example illustrates this idea idea by
1.184 associating common symbols with the constructors of a datatype.
1.185 @@ -211,31 +208,30 @@
1.186 achieves conformance with notational standards of the European
1.187 Commission.
1.188
1.189 - Prefix syntax also works for plain \isakeyword{consts} or
1.190 - \isakeyword{constdefs}, of course.
1.191 + Prefix syntax also works for \isakeyword{consts} or
1.192 + \isakeyword{constdefs}.
1.193 *}
1.194
1.195
1.196 subsection {* Syntax Translations \label{sec:syntax-translations} *}
1.197
1.198 text{*
1.199 - Mixfix syntax annotations work well in those situations where
1.200 - particular constant application forms need to be decorated by
1.201 - concrete syntax; e.g.\ @{text "xor A B"} versus @{text "A \<oplus> B"}
1.202 - covered before. Occasionally the relationship between some piece of
1.203 - notation and its internal form is slightly more involved. Here the
1.204 - concept of \bfindex{syntax translations} enters the scene.
1.205 + Mixfix syntax annotations merely decorate
1.206 + particular constant application forms with
1.207 + concrete syntax, for instance replacing \ @{text "xor A B"} by @{text "A \<oplus> B"}. Occasionally, the relationship between some piece of
1.208 + notation and its internal form is more complicated. Here we need
1.209 + \bfindex{syntax translations}.
1.210
1.211 - Using the raw \isakeyword{syntax}\index{syntax (command)} command we
1.212 - may introduce uninterpreted notational elements, while
1.213 - \commdx{translations} relate input forms with more complex logical
1.214 - expressions. This essentially provides a simple mechanism for
1.215 + Using the \isakeyword{syntax}\index{syntax (command)}, command we
1.216 + introduce uninterpreted notational elements. Then
1.217 + \commdx{translations} relate input forms to complex logical
1.218 + expressions. This provides a simple mechanism for
1.219 syntactic macros; even heavier transformations may be written in ML
1.220 \cite{isabelle-ref}.
1.221
1.222 - \medskip A typical example of syntax translations is to decorate
1.223 - relational expressions (set-membership of tuples) with symbolic
1.224 - notation, e.g.\ @{text "(x, y) \<in> sim"} versus @{text "x \<approx> y"}.
1.225 + \medskip A typical use of syntax translations is to introduce
1.226 + relational notation for membership in a set of pair,
1.227 + replacing \ @{text "(x, y) \<in> sim"} by @{text "x \<approx> y"}.
1.228 *}
1.229
1.230 consts
1.231 @@ -248,7 +244,7 @@
1.232
1.233 text {*
1.234 \noindent Here the name of the dummy constant @{text "_sim"} does
1.235 - not really matter, as long as it is not used elsewhere. Prefixing
1.236 + not matter, as long as it is not used elsewhere. Prefixing
1.237 an underscore is a common convention. The \isakeyword{translations}
1.238 declaration already uses concrete syntax on the left-hand side;
1.239 internally we relate a raw application @{text "_sim x y"} with
1.240 @@ -271,10 +267,11 @@
1.241 replaced by the ``definition'' upon parsing; the effect is reversed
1.242 upon printing.
1.243
1.244 - Simulating definitions via translations is adequate for very basic
1.245 - principles, where a new representation is a trivial variation on an
1.246 + This sort of translation is appropriate when the
1.247 + defined concept is a trivial variation on an
1.248 existing one. On the other hand, syntax translations do not scale
1.249 - up well to large hierarchies of concepts built on each other.
1.250 + up well to large hierarchies of concepts. Translations
1.251 + do not replace definitions!
1.252 *}
1.253
1.254
1.255 @@ -282,7 +279,7 @@
1.256
1.257 text {*
1.258 Isabelle/Isar is centered around the concept of \bfindex{formal
1.259 - proof documents}\index{documents|bold}. The ultimate result of a
1.260 + proof documents}\index{documents|bold}. The outcome of a
1.261 formal development effort is meant to be a human-readable record,
1.262 presented as browsable PDF file or printed on paper. The overall
1.263 document structure follows traditional mathematical articles, with
1.264 @@ -292,8 +289,8 @@
1.265 \medskip The Isabelle document preparation system essentially acts
1.266 as a front-end to {\LaTeX}. After checking specifications and
1.267 proofs formally, the theory sources are turned into typesetting
1.268 - instructions in a schematic manner. This enables users to write
1.269 - authentic reports on theory developments with little effort --- many
1.270 + instructions in a schematic manner. This lets you write
1.271 + authentic reports on theory developments with little effort: many
1.272 technical consistency checks are handled by the system.
1.273
1.274 Here is an example to illustrate the idea of Isabelle document
1.275 @@ -352,8 +349,8 @@
1.276 In contrast to the highly interactive mode of Isabelle/Isar theory
1.277 development, the document preparation stage essentially works in
1.278 batch-mode. An Isabelle \bfindex{session} consists of a collection
1.279 - of source files that may contribute to an output document
1.280 - eventually. Each session is derived from a single parent, usually
1.281 + of source files that may contribute to an output document.
1.282 + Each session is derived from a single parent, usually
1.283 an object-logic image like \texttt{HOL}. This results in an overall
1.284 tree structure, which is reflected by the output location in the
1.285 file system (usually rooted at \verb,~/isabelle/browser_info,).
1.286 @@ -407,14 +404,15 @@
1.287 \item \texttt{IsaMakefile} holds appropriate dependencies and
1.288 invocations of Isabelle tools to control the batch job. In fact,
1.289 several sessions may be managed by the same \texttt{IsaMakefile}.
1.290 - See also \cite{isabelle-sys} for further details, especially on
1.291 + See the \emph{Isabelle System Manual} \cite{isabelle-sys}
1.292 + for further details, especially on
1.293 \texttt{isatool usedir} and \texttt{isatool make}.
1.294
1.295 \end{itemize}
1.296
1.297 One may now start to populate the directory \texttt{MySession}, and
1.298 the file \texttt{MySession/ROOT.ML} accordingly.
1.299 - \texttt{MySession/document/root.tex} should also be adapted at some
1.300 + The file \texttt{MySession/document/root.tex} should also be adapted at some
1.301 point; the default version is mostly self-explanatory. Note that
1.302 \verb,\isabellestyle, enables fine-tuning of the general appearance
1.303 of characters and mathematical symbols (see also
1.304 @@ -423,20 +421,20 @@
1.305 Especially observe the included {\LaTeX} packages \texttt{isabelle}
1.306 (mandatory), \texttt{isabellesym} (required for mathematical
1.307 symbols), and the final \texttt{pdfsetup} (provides sane defaults
1.308 - for \texttt{hyperref}, including URL markup) --- all three are
1.309 + for \texttt{hyperref}, including URL markup). All three are
1.310 distributed with Isabelle. Further packages may be required in
1.311 - particular applications, e.g.\ for unusual mathematical symbols.
1.312 + particular applications, say for unusual mathematical symbols.
1.313
1.314 \medskip Any additional files for the {\LaTeX} stage go into the
1.315 \texttt{MySession/document} directory as well. In particular,
1.316 - adding \texttt{root.bib} (with that specific name) causes an
1.317 + adding a file named \texttt{root.bib} causes an
1.318 automatic run of \texttt{bibtex} to process a bibliographic
1.319 - database; see also \texttt{isatool document} in \cite{isabelle-sys}.
1.320 + database; see also \texttt{isatool document} \cite{isabelle-sys}.
1.321
1.322 \medskip Any failure of the document preparation phase in an
1.323 Isabelle batch session leaves the generated sources in their target
1.324 - location (as pointed out by the accompanied error message). This
1.325 - enables users to trace {\LaTeX} problems with the generated files at
1.326 + location, identified by the accompanying error message. This
1.327 + lets you trace {\LaTeX} problems with the generated files at
1.328 hand.
1.329 *}
1.330
1.331 @@ -505,18 +503,19 @@
1.332 end
1.333 \end{ttbox}
1.334
1.335 - Users may occasionally want to change the meaning of markup
1.336 - commands, say via \verb,\renewcommand, in \texttt{root.tex};
1.337 - \verb,\isamarkupheader, is a good candidate for some tuning, e.g.\
1.338 - moving it up in the hierarchy to become \verb,\chapter,.
1.339 + You may occasionally want to change the meaning of markup
1.340 + commands, say via \verb,\renewcommand, in \texttt{root.tex}. For example,
1.341 + \verb,\isamarkupheader, is a good candidate for some tuning.
1.342 + We could
1.343 + move it up in the hierarchy to become \verb,\chapter,.
1.344
1.345 \begin{verbatim}
1.346 \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
1.347 \end{verbatim}
1.348
1.349 - \noindent That particular modification requires change to the
1.350 + \noindent Now we must change the
1.351 document class given in \texttt{root.tex} to something that supports
1.352 - the notion of chapters in the first place, such as
1.353 + chapters. A suitable command is
1.354 \verb,\documentclass{report},.
1.355
1.356 \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
1.357 @@ -530,7 +529,7 @@
1.358
1.359 \noindent Make sure to include something like
1.360 \verb,\pagestyle{headings}, in \texttt{root.tex}; the document
1.361 - should have more than 2 pages to show the effect.
1.362 + should have more than two pages to show the effect.
1.363 *}
1.364
1.365
1.366 @@ -588,14 +587,14 @@
1.367 \renewcommand{\isastyletxt}{\isastyletext}
1.368 \end{verbatim}
1.369
1.370 - \medskip The $text$ part of each of the various markup commands
1.371 - considered so far essentially inserts \emph{quoted material} into a
1.372 + \medskip The $text$ part of these markup commands
1.373 + essentially inserts \emph{quoted material} into a
1.374 formal text, mainly for instruction of the reader. An
1.375 \bfindex{antiquotation} is again a formal object embedded into such
1.376 an informal portion. The interpretation of antiquotations is
1.377 limited to some well-formedness checks, with the result being pretty
1.378 printed to the resulting document. Quoted text blocks together with
1.379 - antiquotations provide very useful means to reference formal
1.380 + antiquotations provide an attractive means of referring to formal
1.381 entities, with good confidence in getting the technical details
1.382 right (especially syntax and types).
1.383
1.384 @@ -607,32 +606,33 @@
1.385 kind of antiquotation, it generally follows the same conventions for
1.386 types, terms, or theorems as in the formal part of a theory.
1.387
1.388 - \medskip Here is an example of the quotation-antiquotation
1.389 - technique: @{term "%x y. x"} is a well-typed term.
1.390 + \medskip This sentence demonstrates quotations and antiquotations:
1.391 + @{term "%x y. x"} is a well-typed term.
1.392
1.393 - \medskip\noindent The above output has been produced as follows:
1.394 + \medskip\noindent The output above was produced as follows:
1.395 \begin{ttbox}
1.396 text {\ttlbrace}*
1.397 - Here is an example of the quotation-antiquotation technique:
1.398 + This sentence demonstrates quotations and antiquotations:
1.399 {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term.
1.400 *{\ttrbrace}
1.401 \end{ttbox}
1.402
1.403 - From the notational change of the ASCII character \verb,%, to the
1.404 - symbol @{text \<lambda>} we see that the term really got printed by the
1.405 - system (after parsing and type-checking) --- document preparation
1.406 + The notational change from the ASCII character~\verb,%, to the
1.407 + symbol~@{text \<lambda>} reveals that Isabelle printed this term,
1.408 + after parsing and type-checking. Document preparation
1.409 enables symbolic output by default.
1.410
1.411 - \medskip The next example includes an option to modify the
1.412 - \verb,show_types, flag of Isabelle:
1.413 - \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces @{term
1.414 - [show_types] "%x y. x"}. Type-inference has figured out the most
1.415 - general typings in the present (theory) context. Note that term
1.416 - fragments may acquire different typings due to constraints imposed
1.417 - by previous text (say within a proof), e.g.\ due to the main goal
1.418 - statement given beforehand.
1.419 + \medskip The next example includes an option to modify Isabelle's
1.420 + \verb,show_types, flag. The antiquotation
1.421 + \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces
1.422 + the output @{term [show_types] "%x y. x"}.
1.423 + Type inference has figured out the most
1.424 + general typings in the present theory context. Terms
1.425 + may acquire different typings due to constraints imposed
1.426 + by their environment; within a proof, for example, variables are given
1.427 + the same types as they have in the main goal statement.
1.428
1.429 - \medskip Several further kinds of antiquotations (and options) are
1.430 + \medskip Several further kinds of antiquotations and options are
1.431 available \cite{isabelle-sys}. Here are a few commonly used
1.432 combinations:
1.433
1.434 @@ -679,11 +679,11 @@
1.435 Isabelle symbols are the smallest syntactic entities --- a
1.436 straightforward generalization of ASCII characters. While Isabelle
1.437 does not impose any interpretation of the infinite collection of
1.438 - named symbols, {\LaTeX} documents show canonical glyphs for certain
1.439 + named symbols, {\LaTeX} documents use canonical glyphs for certain
1.440 standard symbols \cite[appendix~A]{isabelle-sys}.
1.441
1.442 - The {\LaTeX} code produced from Isabelle text follows a relatively
1.443 - simple scheme. Users may wish to tune the final appearance by
1.444 + The {\LaTeX} code produced from Isabelle text follows a
1.445 + simple scheme. You can tune the final appearance by
1.446 redefining certain macros, say in \texttt{root.tex} of the document.
1.447
1.448 \begin{enumerate}
1.449 @@ -703,8 +703,8 @@
1.450
1.451 \end{enumerate}
1.452
1.453 - Users may occasionally wish to give new {\LaTeX} interpretations of
1.454 - named symbols; this merely requires an appropriate definition of
1.455 + You may occasionally wish to give new {\LaTeX} interpretations of
1.456 + named symbols. This merely requires an appropriate definition of
1.457 \verb,\isasym,$XYZ$\verb,, for \verb,\,\verb,<,$XYZ$\verb,>, (see
1.458 \texttt{isabelle.sty} for working examples). Control symbols are
1.459 slightly more difficult to get right, though.
1.460 @@ -743,17 +743,17 @@
1.461 no_document use_thy "T";
1.462 \end{verbatim}
1.463
1.464 - \medskip Theory output may also be suppressed in smaller portions.
1.465 - For example, research articles, or slides usually do not include the
1.466 + \medskip Theory output may be suppressed more selectively.
1.467 + Research articles and slides usually do not include the
1.468 formal content in full. In order to delimit \bfindex{ignored
1.469 - material} special source comments
1.470 + material}, special source comments
1.471 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
1.472 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), may be included in the
1.473 - text. Only the document preparation system is affected, the formal
1.474 - checking of the theory is performed unchanged.
1.475 + text. Only document preparation is affected; the formal
1.476 + checking of the theory is unchanged.
1.477
1.478 - In the subsequent example we suppress the slightly formalistic
1.479 - \isakeyword{theory} + \isakeyword{end} surroundings a theory.
1.480 + In this example, we suppress a theory's uninteresting
1.481 + \isakeyword{theory} and \isakeyword{end} brackets:
1.482
1.483 \medskip
1.484
1.485 @@ -769,9 +769,9 @@
1.486
1.487 \medskip
1.488
1.489 - Text may be suppressed in a fine-grained manner. We may even drop
1.490 + Text may be suppressed in a fine-grained manner. We may even hide
1.491 vital parts of a proof, pretending that things have been simpler
1.492 - than in reality. For example, this ``fully automatic'' proof is
1.493 + than they really were. For example, this ``fully automatic'' proof is
1.494 actually a fake:
1.495 *}
1.496
1.497 @@ -786,15 +786,14 @@
1.498 \end{verbatim}
1.499 %(*
1.500
1.501 - \medskip Ignoring portions of printed text does demand some care by
1.502 - the writer. First of all, the user is responsible not to obfuscate
1.503 - the underlying theory development in an unduly manner. It is fairly
1.504 - easy to invalidate the visible text, e.g.\ by referencing
1.505 - questionable formal items (strange definitions, arbitrary axioms
1.506 - etc.) that have been hidden from sight beforehand.
1.507 + \medskip Suppressing portions of printed text demands care.
1.508 + You should not misrepresent
1.509 + the underlying theory development. It is
1.510 + easy to invalidate the visible text by hiding
1.511 + references to questionable axioms.
1.512
1.513 Authentic reports of Isabelle/Isar theories, say as part of a
1.514 - library, should refrain from suppressing parts of the text at all.
1.515 + library, should suppress nothing.
1.516 Other users may need the full information for their own derivative
1.517 work. If a particular formalization appears inadequate for general
1.518 public coverage, it is often more appropriate to think of a better
1.519 @@ -802,7 +801,7 @@
1.520
1.521 \medskip Some technical subtleties of the
1.522 \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
1.523 - elements need to be kept in mind, too --- the system performs little
1.524 + elements need to be kept in mind, too --- the system performs few
1.525 sanity checks here. Arguments of markup commands and formal
1.526 comments must not be hidden, otherwise presentation fails. Open and
1.527 close parentheses need to be inserted carefully; it is easy to hide
2.1 --- a/doc-src/TutorialI/Documents/document/Documents.tex Tue Jan 15 10:24:20 2002 +0100
2.2 +++ b/doc-src/TutorialI/Documents/document/Documents.tex Tue Jan 15 13:14:39 2002 +0100
2.3 @@ -8,18 +8,19 @@
2.4 \isamarkuptrue%
2.5 %
2.6 \begin{isamarkuptext}%
2.7 -The core concept of Isabelle's elaborate infrastructure for concrete
2.8 - syntax is that of general \bfindex{mixfix annotations}. Associated
2.9 +The core concept of Isabelle's framework for concrete
2.10 + syntax is that of \bfindex{mixfix annotations}. Associated
2.11 with any kind of constant declaration, mixfixes affect both the
2.12 grammar productions for the parser and output templates for the
2.13 pretty printer.
2.14
2.15 In full generality, parser and pretty printer configuration is a
2.16 - rather subtle affair, see \cite{isabelle-ref} for details. Syntax
2.17 - specifications given by end-users need to interact properly with the
2.18 - existing setup of Isabelle/Pure and Isabelle/HOL. It is
2.19 - particularly important to get the precedence of new syntactic
2.20 - constructs right, avoiding ambiguities with existing elements.
2.21 + subtle affair \cite{isabelle-ref}. Your syntax
2.22 + specifications need to interact properly with the
2.23 + existing setup of Isabelle/Pure and Isabelle/HOL\@.
2.24 + To avoid creating ambiguities with existing elements, it is
2.25 + particularly important to give new syntactic
2.26 + constructs the right precedence.
2.27
2.28 \medskip Subsequently we introduce a few simple syntax declaration
2.29 forms that already cover many common situations fairly well.%
2.30 @@ -31,18 +32,17 @@
2.31 \isamarkuptrue%
2.32 %
2.33 \begin{isamarkuptext}%
2.34 -Syntax annotations may be included wherever constants are declared
2.35 - directly or indirectly, including \isacommand{consts},
2.36 - \isacommand{constdefs}, or \isacommand{datatype} (for the
2.37 - constructor operations). Type-constructors may be annotated as
2.38 +Syntax annotations may be included wherever constants are declared,
2.39 + such as \isacommand{consts} and
2.40 + \isacommand{constdefs} --- and also \isacommand{datatype}, which
2.41 + declares constructor operations. Type-constructors may be annotated as
2.42 well, although this is less frequently encountered in practice (the
2.43 infix type \isa{{\isasymtimes}} comes to mind).
2.44
2.45 Infix declarations\index{infix annotations} provide a useful special
2.46 - case of mixfixes, where users need not care about the full details
2.47 - of priorities, nesting, spacing, etc. The following example of the
2.48 + case of mixfixes. The following example of the
2.49 exclusive-or operation on boolean values illustrates typical infix
2.50 - declarations arising in practice.%
2.51 + declarations.%
2.52 \end{isamarkuptext}%
2.53 \isamarkuptrue%
2.54 \isacommand{constdefs}\isanewline
2.55 @@ -52,16 +52,16 @@
2.56 \begin{isamarkuptext}%
2.57 \noindent Now \isa{xor\ A\ B} and \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} refer to the
2.58 same expression internally. Any curried function with at least two
2.59 - arguments may be associated with infix syntax. For partial
2.60 - applications with less than two operands there is a special notation
2.61 - with \isa{op} prefix: \isa{xor} without arguments is represented
2.62 - as \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}}; together with plain prefix application this
2.63 + arguments may be given infix syntax. For partial
2.64 + applications with fewer than two operands, there is a notation
2.65 + using the prefix~\isa{op}. For instance, \isa{xor} without arguments is represented
2.66 + as \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}}; together with ordinary function application, this
2.67 turns \isa{xor\ A} into \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ A}.
2.68
2.69 \medskip The keyword \isakeyword{infixl} seen above specifies an
2.70 infix operator that is nested to the \emph{left}: in iterated
2.71 applications the more complex expression appears on the left-hand
2.72 - side, \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} stands for \isa{{\isacharparenleft}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B{\isacharparenright}\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C}.
2.73 + side, and \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} stands for \isa{{\isacharparenleft}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B{\isacharparenright}\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C}.
2.74 Similarly, \isakeyword{infixr} specifies nesting to the
2.75 \emph{right}, reading \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}. In contrast, a \emph{non-oriented} declaration via
2.76 \isakeyword{infix} would render \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but
2.77 @@ -69,18 +69,16 @@
2.78
2.79 The string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in our annotation refers to the
2.80 concrete syntax to represent the operator (a literal token), while
2.81 - the number \isa{{\isadigit{6}}{\isadigit{0}}} determines the precedence of the construct
2.82 - (i.e.\ the syntactic priorities of the arguments and result). As it
2.83 - happens, Isabelle/HOL already uses up many popular combinations of
2.84 - ASCII symbols for its own use, including both \isa{{\isacharplus}} and \isa{{\isacharplus}{\isacharplus}}. As a rule of thumb, more awkward character combinations are
2.85 - more likely to be still available for user extensions, just as our
2.86 - present \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}}.
2.87 + the number \isa{{\isadigit{6}}{\isadigit{0}}} determines the precedence of the construct:
2.88 + the syntactic priorities of the arguments and result.
2.89 + Isabelle/HOL already uses up many popular combinations of
2.90 + ASCII symbols for its own use, including both \isa{{\isacharplus}} and \isa{{\isacharplus}{\isacharplus}}. Longer character combinations are
2.91 + more likely to be still available for user extensions, such as our~\isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}}.
2.92
2.93 - Operator precedence also needs some special considerations. The
2.94 - admissible range is 0--1000. Very low or high priorities are
2.95 - basically reserved for the meta-logic. Syntax of Isabelle/HOL
2.96 + Operator precedences have a range of 0--1000. Very low or high priorities are
2.97 + reserved for the meta-logic. HOL syntax
2.98 mainly uses the range of 10--100: the equality infix \isa{{\isacharequal}} is
2.99 - centered at 50, logical connectives (like \isa{{\isasymor}} and \isa{{\isasymand}}) are below 50, and algebraic ones (like \isa{{\isacharplus}} and \isa{{\isacharasterisk}}) above 50. User syntax should strive to coexist with common
2.100 + centered at 50; logical connectives (like \isa{{\isasymor}} and \isa{{\isasymand}}) are below 50; algebraic ones (like \isa{{\isacharplus}} and \isa{{\isacharasterisk}}) are above 50. User syntax should strive to coexist with common
2.101 HOL forms, or use the mostly unused range 100--900.%
2.102 \end{isamarkuptext}%
2.103 \isamarkuptrue%
2.104 @@ -90,8 +88,8 @@
2.105 \isamarkuptrue%
2.106 %
2.107 \begin{isamarkuptext}%
2.108 -Concrete syntax based on plain ASCII characters has its inherent
2.109 - limitations. Rich mathematical notation demands a larger repertoire
2.110 +Concrete syntax based on ASCII characters has inherent
2.111 + limitations. Mathematical notation demands a larger repertoire
2.112 of glyphs. Several standards of extended character sets have been
2.113 proposed over decades, but none has become universally available so
2.114 far. Isabelle supports a generic notion of \bfindex{symbols} as the
2.115 @@ -114,21 +112,20 @@
2.116 interpretation is left to further front-end tools. For example,
2.117 both the user-interface of Proof~General + X-Symbol and the Isabelle
2.118 document processor (see \S\ref{sec:document-preparation}) display
2.119 - the \verb,\,\verb,<forall>, symbol as \isa{{\isasymforall}}.
2.120 + the \verb,\,\verb,<forall>, symbol as~\isa{{\isasymforall}}.
2.121
2.122 A list of standard Isabelle symbols is given in
2.123 - \cite[appendix~A]{isabelle-sys}. Users may introduce their own
2.124 + \cite[appendix~A]{isabelle-sys}. You may introduce their own
2.125 interpretation of further symbols by configuring the appropriate
2.126 front-end tool accordingly, e.g.\ by defining certain {\LaTeX}
2.127 macros (see also \S\ref{sec:doc-prep-symbols}). There are also a
2.128 few predefined control symbols, such as \verb,\,\verb,<^sub>, and
2.129 \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent
2.130 - (printable) symbol, respectively. For example, \verb,A\<^sup>\<star>, is
2.131 + printable symbol, respectively. For example, \verb,A\<^sup>\<star>, is
2.132 output as \isa{A\isactrlsup {\isasymstar}}.
2.133
2.134 - \medskip The following version of our \isa{xor} definition uses a
2.135 - standard Isabelle symbol to achieve typographically more pleasing
2.136 - output than before.%
2.137 + \medskip Replacing our definition of \isa{xor} by the following
2.138 + specifies a Isabelle symbol for the new operator:%
2.139 \end{isamarkuptext}%
2.140 \isamarkuptrue%
2.141 \isamarkupfalse%
2.142 @@ -141,12 +138,12 @@
2.143 \begin{isamarkuptext}%
2.144 \noindent The X-Symbol package within Proof~General provides several
2.145 input methods to enter \isa{{\isasymoplus}} in the text. If all fails one may
2.146 - just type a named entity \verb,\,\verb,<oplus>, by hand; the display
2.147 - will be adapted immediately after continuing input.
2.148 + just type a named entity \verb,\,\verb,<oplus>, by hand; the
2.149 + corresponding symbol will immediately be displayed.
2.150
2.151 - \medskip A slightly more refined scheme of providing alternative
2.152 - syntax forms uses the \bfindex{print mode} concept of Isabelle (see
2.153 - also \cite{isabelle-ref}). By convention, the mode of
2.154 + \medskip More flexible is to provide alternative
2.155 + syntax forms through the \bfindex{print mode} concept~\cite{isabelle-ref}.
2.156 + By convention, the mode of
2.157 ``$xsymbols$'' is enabled whenever Proof~General's X-Symbol mode or
2.158 {\LaTeX} output is active. Now consider the following hybrid
2.159 declaration of \isa{xor}:%
2.160 @@ -173,8 +170,8 @@
2.161 \medskip We may now write \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} or \isa{A\ {\isasymoplus}\ B} in
2.162 input, while output uses the nicer syntax of $xsymbols$, provided
2.163 that print mode is active. Such an arrangement is particularly
2.164 - useful for interactive development, where users may type plain ASCII
2.165 - text, but gain improved visual feedback from the system.%
2.166 + useful for interactive development, where users may type ASCII
2.167 + text and see mathematical symbols displayed during proofs.%
2.168 \end{isamarkuptext}%
2.169 \isamarkuptrue%
2.170 %
2.171 @@ -184,7 +181,7 @@
2.172 %
2.173 \begin{isamarkuptext}%
2.174 Prefix syntax annotations\index{prefix annotation} are another
2.175 - degenerate form of mixfixes \cite{isabelle-ref}, without any
2.176 + form of mixfixes \cite{isabelle-ref}, without any
2.177 template arguments or priorities --- just some bits of literal
2.178 syntax. The following example illustrates this idea idea by
2.179 associating common symbols with the constructors of a datatype.%
2.180 @@ -206,8 +203,8 @@
2.181 achieves conformance with notational standards of the European
2.182 Commission.
2.183
2.184 - Prefix syntax also works for plain \isakeyword{consts} or
2.185 - \isakeyword{constdefs}, of course.%
2.186 + Prefix syntax also works for \isakeyword{consts} or
2.187 + \isakeyword{constdefs}.%
2.188 \end{isamarkuptext}%
2.189 \isamarkuptrue%
2.190 %
2.191 @@ -216,23 +213,22 @@
2.192 \isamarkuptrue%
2.193 %
2.194 \begin{isamarkuptext}%
2.195 -Mixfix syntax annotations work well in those situations where
2.196 - particular constant application forms need to be decorated by
2.197 - concrete syntax; e.g.\ \isa{xor\ A\ B} versus \isa{A\ {\isasymoplus}\ B}
2.198 - covered before. Occasionally the relationship between some piece of
2.199 - notation and its internal form is slightly more involved. Here the
2.200 - concept of \bfindex{syntax translations} enters the scene.
2.201 +Mixfix syntax annotations merely decorate
2.202 + particular constant application forms with
2.203 + concrete syntax, for instance replacing \ \isa{xor\ A\ B} by \isa{A\ {\isasymoplus}\ B}. Occasionally, the relationship between some piece of
2.204 + notation and its internal form is more complicated. Here we need
2.205 + \bfindex{syntax translations}.
2.206
2.207 - Using the raw \isakeyword{syntax}\index{syntax (command)} command we
2.208 - may introduce uninterpreted notational elements, while
2.209 - \commdx{translations} relate input forms with more complex logical
2.210 - expressions. This essentially provides a simple mechanism for
2.211 + Using the \isakeyword{syntax}\index{syntax (command)}, command we
2.212 + introduce uninterpreted notational elements. Then
2.213 + \commdx{translations} relate input forms to complex logical
2.214 + expressions. This provides a simple mechanism for
2.215 syntactic macros; even heavier transformations may be written in ML
2.216 \cite{isabelle-ref}.
2.217
2.218 - \medskip A typical example of syntax translations is to decorate
2.219 - relational expressions (set-membership of tuples) with symbolic
2.220 - notation, e.g.\ \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} versus \isa{x\ {\isasymapprox}\ y}.%
2.221 + \medskip A typical use of syntax translations is to introduce
2.222 + relational notation for membership in a set of pair,
2.223 + replacing \ \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} by \isa{x\ {\isasymapprox}\ y}.%
2.224 \end{isamarkuptext}%
2.225 \isamarkuptrue%
2.226 \isacommand{consts}\isanewline
2.227 @@ -247,7 +243,7 @@
2.228 %
2.229 \begin{isamarkuptext}%
2.230 \noindent Here the name of the dummy constant \isa{{\isacharunderscore}sim} does
2.231 - not really matter, as long as it is not used elsewhere. Prefixing
2.232 + not matter, as long as it is not used elsewhere. Prefixing
2.233 an underscore is a common convention. The \isakeyword{translations}
2.234 declaration already uses concrete syntax on the left-hand side;
2.235 internally we relate a raw application \isa{{\isacharunderscore}sim\ x\ y} with
2.236 @@ -271,10 +267,11 @@
2.237 replaced by the ``definition'' upon parsing; the effect is reversed
2.238 upon printing.
2.239
2.240 - Simulating definitions via translations is adequate for very basic
2.241 - principles, where a new representation is a trivial variation on an
2.242 + This sort of translation is appropriate when the
2.243 + defined concept is a trivial variation on an
2.244 existing one. On the other hand, syntax translations do not scale
2.245 - up well to large hierarchies of concepts built on each other.%
2.246 + up well to large hierarchies of concepts. Translations
2.247 + do not replace definitions!%
2.248 \end{isamarkuptext}%
2.249 \isamarkuptrue%
2.250 %
2.251 @@ -284,7 +281,7 @@
2.252 %
2.253 \begin{isamarkuptext}%
2.254 Isabelle/Isar is centered around the concept of \bfindex{formal
2.255 - proof documents}\index{documents|bold}. The ultimate result of a
2.256 + proof documents}\index{documents|bold}. The outcome of a
2.257 formal development effort is meant to be a human-readable record,
2.258 presented as browsable PDF file or printed on paper. The overall
2.259 document structure follows traditional mathematical articles, with
2.260 @@ -294,8 +291,8 @@
2.261 \medskip The Isabelle document preparation system essentially acts
2.262 as a front-end to {\LaTeX}. After checking specifications and
2.263 proofs formally, the theory sources are turned into typesetting
2.264 - instructions in a schematic manner. This enables users to write
2.265 - authentic reports on theory developments with little effort --- many
2.266 + instructions in a schematic manner. This lets you write
2.267 + authentic reports on theory developments with little effort: many
2.268 technical consistency checks are handled by the system.
2.269
2.270 Here is an example to illustrate the idea of Isabelle document
2.271 @@ -362,8 +359,8 @@
2.272 In contrast to the highly interactive mode of Isabelle/Isar theory
2.273 development, the document preparation stage essentially works in
2.274 batch-mode. An Isabelle \bfindex{session} consists of a collection
2.275 - of source files that may contribute to an output document
2.276 - eventually. Each session is derived from a single parent, usually
2.277 + of source files that may contribute to an output document.
2.278 + Each session is derived from a single parent, usually
2.279 an object-logic image like \texttt{HOL}. This results in an overall
2.280 tree structure, which is reflected by the output location in the
2.281 file system (usually rooted at \verb,~/isabelle/browser_info,).
2.282 @@ -417,14 +414,15 @@
2.283 \item \texttt{IsaMakefile} holds appropriate dependencies and
2.284 invocations of Isabelle tools to control the batch job. In fact,
2.285 several sessions may be managed by the same \texttt{IsaMakefile}.
2.286 - See also \cite{isabelle-sys} for further details, especially on
2.287 + See the \emph{Isabelle System Manual} \cite{isabelle-sys}
2.288 + for further details, especially on
2.289 \texttt{isatool usedir} and \texttt{isatool make}.
2.290
2.291 \end{itemize}
2.292
2.293 One may now start to populate the directory \texttt{MySession}, and
2.294 the file \texttt{MySession/ROOT.ML} accordingly.
2.295 - \texttt{MySession/document/root.tex} should also be adapted at some
2.296 + The file \texttt{MySession/document/root.tex} should also be adapted at some
2.297 point; the default version is mostly self-explanatory. Note that
2.298 \verb,\isabellestyle, enables fine-tuning of the general appearance
2.299 of characters and mathematical symbols (see also
2.300 @@ -433,20 +431,20 @@
2.301 Especially observe the included {\LaTeX} packages \texttt{isabelle}
2.302 (mandatory), \texttt{isabellesym} (required for mathematical
2.303 symbols), and the final \texttt{pdfsetup} (provides sane defaults
2.304 - for \texttt{hyperref}, including URL markup) --- all three are
2.305 + for \texttt{hyperref}, including URL markup). All three are
2.306 distributed with Isabelle. Further packages may be required in
2.307 - particular applications, e.g.\ for unusual mathematical symbols.
2.308 + particular applications, say for unusual mathematical symbols.
2.309
2.310 \medskip Any additional files for the {\LaTeX} stage go into the
2.311 \texttt{MySession/document} directory as well. In particular,
2.312 - adding \texttt{root.bib} (with that specific name) causes an
2.313 + adding a file named \texttt{root.bib} causes an
2.314 automatic run of \texttt{bibtex} to process a bibliographic
2.315 - database; see also \texttt{isatool document} in \cite{isabelle-sys}.
2.316 + database; see also \texttt{isatool document} \cite{isabelle-sys}.
2.317
2.318 \medskip Any failure of the document preparation phase in an
2.319 Isabelle batch session leaves the generated sources in their target
2.320 - location (as pointed out by the accompanied error message). This
2.321 - enables users to trace {\LaTeX} problems with the generated files at
2.322 + location, identified by the accompanying error message. This
2.323 + lets you trace {\LaTeX} problems with the generated files at
2.324 hand.%
2.325 \end{isamarkuptext}%
2.326 \isamarkuptrue%
2.327 @@ -517,18 +515,19 @@
2.328 end
2.329 \end{ttbox}
2.330
2.331 - Users may occasionally want to change the meaning of markup
2.332 - commands, say via \verb,\renewcommand, in \texttt{root.tex};
2.333 - \verb,\isamarkupheader, is a good candidate for some tuning, e.g.\
2.334 - moving it up in the hierarchy to become \verb,\chapter,.
2.335 + You may occasionally want to change the meaning of markup
2.336 + commands, say via \verb,\renewcommand, in \texttt{root.tex}. For example,
2.337 + \verb,\isamarkupheader, is a good candidate for some tuning.
2.338 + We could
2.339 + move it up in the hierarchy to become \verb,\chapter,.
2.340
2.341 \begin{verbatim}
2.342 \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
2.343 \end{verbatim}
2.344
2.345 - \noindent That particular modification requires change to the
2.346 + \noindent Now we must change the
2.347 document class given in \texttt{root.tex} to something that supports
2.348 - the notion of chapters in the first place, such as
2.349 + chapters. A suitable command is
2.350 \verb,\documentclass{report},.
2.351
2.352 \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
2.353 @@ -542,7 +541,7 @@
2.354
2.355 \noindent Make sure to include something like
2.356 \verb,\pagestyle{headings}, in \texttt{root.tex}; the document
2.357 - should have more than 2 pages to show the effect.%
2.358 + should have more than two pages to show the effect.%
2.359 \end{isamarkuptext}%
2.360 \isamarkuptrue%
2.361 %
2.362 @@ -612,14 +611,14 @@
2.363 \renewcommand{\isastyletxt}{\isastyletext}
2.364 \end{verbatim}
2.365
2.366 - \medskip The $text$ part of each of the various markup commands
2.367 - considered so far essentially inserts \emph{quoted material} into a
2.368 + \medskip The $text$ part of these markup commands
2.369 + essentially inserts \emph{quoted material} into a
2.370 formal text, mainly for instruction of the reader. An
2.371 \bfindex{antiquotation} is again a formal object embedded into such
2.372 an informal portion. The interpretation of antiquotations is
2.373 limited to some well-formedness checks, with the result being pretty
2.374 printed to the resulting document. Quoted text blocks together with
2.375 - antiquotations provide very useful means to reference formal
2.376 + antiquotations provide an attractive means of referring to formal
2.377 entities, with good confidence in getting the technical details
2.378 right (especially syntax and types).
2.379
2.380 @@ -631,31 +630,33 @@
2.381 kind of antiquotation, it generally follows the same conventions for
2.382 types, terms, or theorems as in the formal part of a theory.
2.383
2.384 - \medskip Here is an example of the quotation-antiquotation
2.385 - technique: \isa{{\isasymlambda}x\ y{\isachardot}\ x} is a well-typed term.
2.386 + \medskip This sentence demonstrates quotations and antiquotations:
2.387 + \isa{{\isasymlambda}x\ y{\isachardot}\ x} is a well-typed term.
2.388
2.389 - \medskip\noindent The above output has been produced as follows:
2.390 + \medskip\noindent The output above was produced as follows:
2.391 \begin{ttbox}
2.392 text {\ttlbrace}*
2.393 - Here is an example of the quotation-antiquotation technique:
2.394 + This sentence demonstrates quotations and antiquotations:
2.395 {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term.
2.396 *{\ttrbrace}
2.397 \end{ttbox}
2.398
2.399 - From the notational change of the ASCII character \verb,%, to the
2.400 - symbol \isa{{\isasymlambda}} we see that the term really got printed by the
2.401 - system (after parsing and type-checking) --- document preparation
2.402 + The notational change from the ASCII character~\verb,%, to the
2.403 + symbol~\isa{{\isasymlambda}} reveals that Isabelle printed this term,
2.404 + after parsing and type-checking. Document preparation
2.405 enables symbolic output by default.
2.406
2.407 - \medskip The next example includes an option to modify the
2.408 - \verb,show_types, flag of Isabelle:
2.409 - \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces \isa{{\isasymlambda}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ y{\isasymColon}{\isacharprime}b{\isachardot}\ x}. Type-inference has figured out the most
2.410 - general typings in the present (theory) context. Note that term
2.411 - fragments may acquire different typings due to constraints imposed
2.412 - by previous text (say within a proof), e.g.\ due to the main goal
2.413 - statement given beforehand.
2.414 + \medskip The next example includes an option to modify Isabelle's
2.415 + \verb,show_types, flag. The antiquotation
2.416 + \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces
2.417 + the output \isa{{\isasymlambda}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ y{\isasymColon}{\isacharprime}b{\isachardot}\ x}.
2.418 + Type inference has figured out the most
2.419 + general typings in the present theory context. Terms
2.420 + may acquire different typings due to constraints imposed
2.421 + by their environment; within a proof, for example, variables are given
2.422 + the same types as they have in the main goal statement.
2.423
2.424 - \medskip Several further kinds of antiquotations (and options) are
2.425 + \medskip Several further kinds of antiquotations and options are
2.426 available \cite{isabelle-sys}. Here are a few commonly used
2.427 combinations:
2.428
2.429 @@ -703,11 +704,11 @@
2.430 Isabelle symbols are the smallest syntactic entities --- a
2.431 straightforward generalization of ASCII characters. While Isabelle
2.432 does not impose any interpretation of the infinite collection of
2.433 - named symbols, {\LaTeX} documents show canonical glyphs for certain
2.434 + named symbols, {\LaTeX} documents use canonical glyphs for certain
2.435 standard symbols \cite[appendix~A]{isabelle-sys}.
2.436
2.437 - The {\LaTeX} code produced from Isabelle text follows a relatively
2.438 - simple scheme. Users may wish to tune the final appearance by
2.439 + The {\LaTeX} code produced from Isabelle text follows a
2.440 + simple scheme. You can tune the final appearance by
2.441 redefining certain macros, say in \texttt{root.tex} of the document.
2.442
2.443 \begin{enumerate}
2.444 @@ -727,8 +728,8 @@
2.445
2.446 \end{enumerate}
2.447
2.448 - Users may occasionally wish to give new {\LaTeX} interpretations of
2.449 - named symbols; this merely requires an appropriate definition of
2.450 + You may occasionally wish to give new {\LaTeX} interpretations of
2.451 + named symbols. This merely requires an appropriate definition of
2.452 \verb,\isasym,$XYZ$\verb,, for \verb,\,\verb,<,$XYZ$\verb,>, (see
2.453 \texttt{isabelle.sty} for working examples). Control symbols are
2.454 slightly more difficult to get right, though.
2.455 @@ -769,17 +770,17 @@
2.456 no_document use_thy "T";
2.457 \end{verbatim}
2.458
2.459 - \medskip Theory output may also be suppressed in smaller portions.
2.460 - For example, research articles, or slides usually do not include the
2.461 + \medskip Theory output may be suppressed more selectively.
2.462 + Research articles and slides usually do not include the
2.463 formal content in full. In order to delimit \bfindex{ignored
2.464 - material} special source comments
2.465 + material}, special source comments
2.466 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
2.467 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), may be included in the
2.468 - text. Only the document preparation system is affected, the formal
2.469 - checking of the theory is performed unchanged.
2.470 + text. Only document preparation is affected; the formal
2.471 + checking of the theory is unchanged.
2.472
2.473 - In the subsequent example we suppress the slightly formalistic
2.474 - \isakeyword{theory} + \isakeyword{end} surroundings a theory.
2.475 + In this example, we suppress a theory's uninteresting
2.476 + \isakeyword{theory} and \isakeyword{end} brackets:
2.477
2.478 \medskip
2.479
2.480 @@ -795,9 +796,9 @@
2.481
2.482 \medskip
2.483
2.484 - Text may be suppressed in a fine-grained manner. We may even drop
2.485 + Text may be suppressed in a fine-grained manner. We may even hide
2.486 vital parts of a proof, pretending that things have been simpler
2.487 - than in reality. For example, this ``fully automatic'' proof is
2.488 + than they really were. For example, this ``fully automatic'' proof is
2.489 actually a fake:%
2.490 \end{isamarkuptext}%
2.491 \isamarkuptrue%
2.492 @@ -813,15 +814,14 @@
2.493 \end{verbatim}
2.494 %(*
2.495
2.496 - \medskip Ignoring portions of printed text does demand some care by
2.497 - the writer. First of all, the user is responsible not to obfuscate
2.498 - the underlying theory development in an unduly manner. It is fairly
2.499 - easy to invalidate the visible text, e.g.\ by referencing
2.500 - questionable formal items (strange definitions, arbitrary axioms
2.501 - etc.) that have been hidden from sight beforehand.
2.502 + \medskip Suppressing portions of printed text demands care.
2.503 + You should not misrepresent
2.504 + the underlying theory development. It is
2.505 + easy to invalidate the visible text by hiding
2.506 + references to questionable axioms.
2.507
2.508 Authentic reports of Isabelle/Isar theories, say as part of a
2.509 - library, should refrain from suppressing parts of the text at all.
2.510 + library, should suppress nothing.
2.511 Other users may need the full information for their own derivative
2.512 work. If a particular formalization appears inadequate for general
2.513 public coverage, it is often more appropriate to think of a better
2.514 @@ -829,7 +829,7 @@
2.515
2.516 \medskip Some technical subtleties of the
2.517 \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
2.518 - elements need to be kept in mind, too --- the system performs little
2.519 + elements need to be kept in mind, too --- the system performs few
2.520 sanity checks here. Arguments of markup commands and formal
2.521 comments must not be hidden, otherwise presentation fails. Open and
2.522 close parentheses need to be inserted carefully; it is easy to hide
3.1 --- a/doc-src/TutorialI/Documents/documents.tex Tue Jan 15 10:24:20 2002 +0100
3.2 +++ b/doc-src/TutorialI/Documents/documents.tex Tue Jan 15 13:14:39 2002 +0100
3.3 @@ -3,13 +3,13 @@
3.4 \label{ch:thy-present}
3.5
3.6 By now the reader should have become sufficiently acquainted with elementary
3.7 -theory development in Isabelle/HOL. The following interlude covers the
3.8 -seemingly ``marginal'' issue of presenting theories in a typographically
3.9 +theory development in Isabelle/HOL\@. The following interlude describes
3.10 +how to present theories in a typographically
3.11 pleasing manner. Isabelle provides a rich infrastructure for concrete syntax
3.12 of the underlying $\lambda$-calculus language (see
3.13 -\S\ref{sec:concrete-syntax}), as well as document preparation of theory texts
3.14 +{\S}\ref{sec:concrete-syntax}), as well as document preparation of theory texts
3.15 based on existing PDF-{\LaTeX} technology (see
3.16 -\S\ref{sec:document-preparation}).
3.17 +{\S}\ref{sec:document-preparation}).
3.18
3.19 As pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than 300
3.20 years ago, \emph{notions} are in principle more important than