--- a/doc-src/TutorialI/Documents/document/Documents.tex Tue Jan 08 17:32:28 2002 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Tue Jan 08 17:32:40 2002 +0100
@@ -15,14 +15,14 @@
parser and output templates for the pretty printer.
In full generality, the whole affair of parser and pretty printer
- configuration is rather subtle, see also \cite{isabelle-ref}. Any
- syntax specifications given by end-users need to interact properly
+ configuration is rather subtle, see also \cite{isabelle-ref}.
+ Syntax specifications given by end-users need to interact properly
with the existing setup of Isabelle/Pure and Isabelle/HOL. It is
particularly important to get the precedence of new syntactic
constructs right, avoiding ambiguities with existing elements.
- \medskip Subsequently we introduce a few simple declaration forms
- that already cover the most common situations fairly well.%
+ \medskip Subsequently we introduce a few simple syntax declaration
+ forms that already cover most common situations fairly well.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -78,15 +78,15 @@
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
HOL forms, or use the mostly unused range 100--900.
- The keyword \isakeyword{infixl} specifies an operator that is nested
- to the \emph{left}: in iterated applications the more complex
+ The keyword \isakeyword{infixl} specifies an infix operator that is
+ nested to the \emph{left}: in iterated applications the more complex
expression appears on the left-hand 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}. Similarly,
\isakeyword{infixr} specifies to nesting to the \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 \isakeyword{infix}
- would have rendered \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but demand
- explicit parentheses about the intended grouping.%
+ would render \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but demand explicit
+ parentheses to indicate the intended grouping.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -97,7 +97,7 @@
\begin{isamarkuptext}%
Concrete syntax based on plain ASCII characters has its inherent
limitations. Rich mathematical notation demands a larger repertoire
- of symbols. Several standards of extended character sets have been
+ of glyphs. Several standards of extended character sets have been
proposed over decades, but none has become universally available so
far. Isabelle supports a generic notion of \bfindex{symbols} as the
smallest entities of source text, without referring to internal
@@ -117,9 +117,9 @@
Here $ident$ may be any identifier according to the usual Isabelle
conventions. This results in an infinite store of symbols, whose
interpretation is left to further front-end tools. For example,
- both by the user-interface of Proof~General + X-Symbol and the
- Isabelle document processor (see \S\ref{sec:document-preparation})
- display the \verb,\,\verb,<forall>, symbol really as \isa{{\isasymforall}}.
+ both the user-interface of Proof~General + X-Symbol and the Isabelle
+ document processor (see \S\ref{sec:document-preparation}) display
+ the \verb,\,\verb,<forall>, symbol really as \isa{{\isasymforall}}.
A list of standard Isabelle symbols is given in
\cite[appendix~A]{isabelle-sys}. Users may introduce their own
@@ -129,10 +129,11 @@
few predefined control symbols, such as \verb,\,\verb,<^sub>, and
\verb,\,\verb,<^sup>, for sub- and superscript of the subsequent
(printable) symbol, respectively. For example, \verb,A\<^sup>\<star>, is
- shown as \isa{A\isactrlsup {\isasymstar}}.
+ output as \isa{A\isactrlsup {\isasymstar}}.
\medskip The following version of our \isa{xor} definition uses a
- standard Isabelle symbol to achieve typographically pleasing output.%
+ standard Isabelle symbol to achieve typographically more pleasing
+ output than before.%
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
@@ -145,14 +146,14 @@
\begin{isamarkuptext}%
\noindent The X-Symbol package within Proof~General provides several
input methods to enter \isa{{\isasymoplus}} in the text. If all fails one may
- just type \verb,\,\verb,<oplus>, by hand; the display will be
- adapted immediately after continuing input.
+ just type a named entity \verb,\,\verb,<oplus>, by hand; the display
+ will be adapted immediately after continuing input.
\medskip A slightly more refined scheme is to provide alternative
syntax via the \bfindex{print mode} concept of Isabelle (see also
\cite{isabelle-ref}). By convention, the mode of ``$xsymbols$'' is
enabled whenever Proof~General's X-Symbol mode (or {\LaTeX} output)
- is active. Consider the following hybrid declaration of \isa{xor}.%
+ is active. Now consider the following hybrid declaration of \isa{xor}.%
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
@@ -170,15 +171,14 @@
The \commdx{syntax} command introduced here acts like
\isakeyword{consts}, but without declaring a logical constant; an
optional print mode specification may be given, too. Note that the
- type declaration given here merely serves for syntactic purposes,
+ type declaration given above merely serves for syntactic purposes,
and is not checked for consistency with the real constant.
- \medskip We may now write either \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} or \isa{{\isasymoplus}} in
- input, while output uses the nicer syntax of $xsymbols$, provided
- that print mode is presently active. Such an arrangement is
+ \medskip We may now write either \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} or \isa{A\ {\isasymoplus}\ B} in input, while output uses the nicer syntax of $xsymbols$,
+ provided that print mode is active. Such an arrangement is
particularly useful for interactive development, where users may
type plain ASCII text, but gain improved visual feedback from the
- system (say in current goal output).
+ system.
\begin{warn}
Alternative syntax declarations are apt to result in varying
@@ -192,7 +192,7 @@
\medskip The following variant makes the alternative \isa{{\isasymoplus}}
notation only available for output. Thus we may enforce input
sources to refer to plain ASCII only, but effectively disable
- cut-and-paste from output as well.%
+ cut-and-paste from output at the same time.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{syntax}\ {\isacharparenleft}xsymbols\ \isakeyword{output}{\isacharparenright}\isanewline
@@ -204,7 +204,7 @@
%
\begin{isamarkuptext}%
Prefix syntax annotations\index{prefix annotation} are just another
- degenerate form of general mixfixes \cite{isabelle-ref}, without any
+ degenerate form of mixfixes \cite{isabelle-ref}, without any
template arguments or priorities --- just some bits of literal
syntax. The following example illustrates this idea idea by
associating common symbols with the constructors of a datatype.%
@@ -235,18 +235,18 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Mixfix syntax annotations work well for those situations where a
+Mixfix syntax annotations work well in those situations where
particular constant application forms need to be decorated by
- concrete syntax; just reconsider \isa{xor\ A\ B} versus \isa{A\ {\isasymoplus}\ B} covered before. Occasionally, the relationship between some
+ concrete syntax; just reconsider \isa{xor\ A\ B} versus \isa{A\ {\isasymoplus}\ B} covered before. Occasionally the relationship between some
piece of notation and its internal form is slightly more involved.
Here the concept of \bfindex{syntax translations} enters the scene.
Using the raw \isakeyword{syntax}\index{syntax (command)} command we
may introduce uninterpreted notational elements, while
- \commdx{translations} relates the input forms with more complex
- logical expressions. This essentially provides a simple mechanism
- for for syntactic macros; even heavier transformations may be
- written in ML \cite{isabelle-ref}.
+ \commdx{translations} relates input forms with more complex logical
+ expressions. This essentially provides a simple mechanism for
+ syntactic macros; even heavier transformations may be written in ML
+ \cite{isabelle-ref}.
\medskip A typical example of syntax translations is to decorate
relational expressions with nice symbolic notation, such as \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} versus \isa{x\ {\isasymapprox}\ y}.%
@@ -319,11 +319,11 @@
\S\ref{sec:doc-prep-suppress}).
\medskip The Isabelle document preparation system essentially acts
- like a formal front-end to {\LaTeX}. After checking specifications
- and proofs, the theory sources are turned into typesetting
- instructions in a well-defined manner. This enables users to write
- authentic reports on formal developments with little effort, most
- tedious consistency checks are handled by the system.%
+ as a front-end to {\LaTeX}. After checking specifications and
+ proofs formally, the theory sources are turned into typesetting
+ instructions in a schematic manner. This enables users to write
+ authentic reports on theory developments with little effort, where
+ most consistency checks are handled by the system.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -334,26 +334,25 @@
\begin{isamarkuptext}%
In contrast to the highly interactive mode of Isabelle/Isar theory
development, the document preparation stage essentially works in
- batch-mode. An Isabelle \bfindex{session} essentially consists of a
- collection of theory source files that contribute to a single output
- document eventually. Session is derived from a single parent each
- (usually an object-logic image like \texttt{HOL}), resulting in an
- overall tree structure that is reflected in the output location
- within the file system (usually rooted at
- \verb,~/isabelle/browser_info,).
+ batch-mode. An Isabelle \bfindex{session} consists of a collection
+ of theory source files that contribute to a single output document
+ eventually. Each session is derived from a single parent one,
+ usually an object-logic image like \texttt{HOL}. This results in an
+ overall tree structure, which is reflected by the output location in
+ the file system (usually rooted at \verb,~/isabelle/browser_info,).
- Here is the canonical arrangement of sources of a session called
- \texttt{MySession}:
+ \medskip Here is the canonical arrangement of sources of a session
+ called \texttt{MySession}:
\begin{itemize}
- \item Directory \texttt{MySession} contains the required theory
- files $T@1$\texttt{.thy}, \dots, $T@n$\texttt{.thy}.
+ \item Directory \texttt{MySession} holds the required theory files
+ $T@1$\texttt{.thy}, \dots, $T@n$\texttt{.thy}.
\item File \texttt{MySession/ROOT.ML} holds appropriate ML commands
for loading all wanted theories, usually just
``\texttt{use_thy"$T@i$";}'' for any $T@i$ in leaf position of the
- theory dependency graph.
+ dependency graph.
\item Directory \texttt{MySession/document} contains everything
required for the {\LaTeX} stage; only \texttt{root.tex} needs to be
@@ -362,9 +361,9 @@
The latter file holds appropriate {\LaTeX} code to commence a
document (\verb,\documentclass, etc.), and to include the generated
files $T@i$\texttt{.tex} for each theory. The generated
- \texttt{session.tex} will hold {\LaTeX} commands to include all
+ \texttt{session.tex} will contain {\LaTeX} commands to include all
theory output files in topologically sorted order, so
- \verb,\input{session}, in \texttt{root.tex} will do it in most
+ \verb,\input{session}, in \texttt{root.tex} does the job in most
situations.
\item \texttt{IsaMakefile} outside of the directory
@@ -382,7 +381,7 @@
\medskip In reality, users may want to have \texttt{isatool mkdir}
generate an initial working setup without further ado. For example,
- an empty session \texttt{MySession} derived from \texttt{HOL} may be
+ a new session \texttt{MySession} derived from \texttt{HOL} may be
produced as follows:
\begin{verbatim}
@@ -392,42 +391,41 @@
This processes the session with sensible default options, including
verbose mode to tell the user where the ultimate results will
- appear. The above dry run should produce should already be able to
- produce a single page of output (with a dummy title, empty table of
- contents etc.). Any failure at that stage is likely to indicate
- technical problems with the user's {\LaTeX}
- installation.\footnote{Especially make sure that \texttt{pdflatex}
- is present; if all fails one may fall back on DVI output by changing
- \texttt{usedir} options \cite{isabelle-sys}.}
+ appear. The above dry run should already be able to produce a
+ single page of output (with a dummy title, empty table of contents
+ etc.). Any failure at that stage is likely to indicate technical
+ problems with the user's {\LaTeX} installation.\footnote{Especially
+ make sure that \texttt{pdflatex} is present; if all fails one may
+ fall back on DVI output by changing \texttt{usedir} options in
+ \texttt{IsaMakefile} \cite{isabelle-sys}.}
\medskip One may now start to populate the directory
\texttt{MySession}, and the file \texttt{MySession/ROOT.ML}
accordingly. \texttt{MySession/document/root.tex} should be also
adapted at some point; the default version is mostly
- self-explanatory. Note that the \verb,\isabellestyle, enables
+ self-explanatory. Note that \verb,\isabellestyle, enables
fine-tuning of the general appearance of characters and mathematical
symbols (see also \S\ref{sec:doc-prep-symbols}).
- Especially note the standard inclusion of {\LaTeX} packages
+ Especially observe inclusion of the {\LaTeX} packages
\texttt{isabelle} (mandatory), and \texttt{isabellesym} (required
for mathematical symbols), and the final \texttt{pdfsetup} (provides
handsome defaults for \texttt{hyperref}, including URL markup).
- Further {\LaTeX} packages further packages may required in
- particular applications, e.g.\ for unusual Isabelle symbols.
+ Further packages may be required in particular applications, e.g.\
+ for unusual Isabelle symbols.
- \medskip Further auxiliary files for the {\LaTeX} stage should be
- included in the \texttt{MySession/document} directory, e.g.\
- additional {\TeX} sources or graphics. In particular, adding
- \texttt{root.bib} here (with that specific name) causes an automatic
- run of \texttt{bibtex} to process a bibliographic database; see for
- further commodities \texttt{isatool document} covered in
- \cite{isabelle-sys}.
+ \medskip Additional files for the {\LaTeX} stage should be included
+ in the \texttt{MySession/document} directory, e.g.\ further {\TeX}
+ sources or graphics. In particular, adding \texttt{root.bib} here
+ (with that specific name) causes an automatic run of \texttt{bibtex}
+ to process a bibliographic database; see also \texttt{isatool
+ document} covered in \cite{isabelle-sys}.
\medskip Any failure of the document preparation phase in an
- Isabelle batch session leaves the generated sources in there target
- location (as pointed out by the accompanied error message). In case
- of {\LaTeX} errors, users may trace error messages at the file
- position of the generated text.%
+ Isabelle batch session leaves the generated sources in their target
+ location (as pointed out by the accompanied error message). This
+ enables users to trace {\LaTeX} at the file positions of the
+ generated material.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -499,7 +497,7 @@
Users may occasionally want to change the meaning of markup
commands, say via \verb,\renewcommand, in \texttt{root.tex};
- \verb,\isamarkupheader, is a good candidate for some adaption, e.g.\
+ \verb,\isamarkupheader, is a good candidate for some tuning, e.g.\
moving it up in the hierarchy to become \verb,\chapter,.
\begin{verbatim}
@@ -541,10 +539,11 @@
theory or proof context (\bfindex{text blocks}).
\medskip Marginal comments are part of each command's concrete
- syntax \cite{isabelle-ref}; the common form is ``\verb,--,~text''
+ syntax \cite{isabelle-ref}; the common form is ``\verb,--,~$text$''
where $text$ is delimited by \verb,",\dots\verb,", or
- \verb,{,\verb,*,~\dots~\verb,*,\verb,}, as usual. Multiple marginal
- comments may be given at the same time. Here is a simple example:%
+ \verb,{,\verb,*,~\dots~\verb,*,\verb,}, as before. Multiple
+ marginal comments may be given at the same time. Here is a simple
+ example:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ {\isachardoublequote}A\ {\isacharminus}{\isacharminus}{\isachargreater}\ A{\isachardoublequote}\isanewline
@@ -572,40 +571,39 @@
by (rule impI) -- "implicit assumption step involved here"
\end{verbatim}
- From the {\LaTeX} view, ``\verb,--,'' acts like a markup command,
- the corresponding macro is \verb,\isamarkupcmt, (with a single
- argument).
+ From the {\LaTeX} viewpoint, ``\verb,--,'' acts like a markup
+ command, associated with the macro \verb,\isamarkupcmt, (taking a
+ single argument).
\medskip Text blocks are introduced by the commands \bfindex{text}
and \bfindex{txt}, for theory and proof contexts, respectively.
Each takes again a single $text$ argument, which is interpreted as a
free-form paragraph in {\LaTeX} (surrounded by some additional
- vertical space). The exact behavior may be changed by redefining
- the {\LaTeX} environments of \verb,isamarkuptext, or
- \verb,isamarkuptxt,, respectively. The text style of the body is
- determined by the \verb,\isastyletext, and \verb,\isastyletxt,
- macros; the default uses a smaller font within proofs.
+ vertical space). This behavior may be changed by redefining the
+ {\LaTeX} environments of \verb,isamarkuptext, or
+ \verb,isamarkuptxt,, respectively (via \verb,\renewenvironment,) The
+ text style of the body is determined by \verb,\isastyletext, and
+ \verb,\isastyletxt,; the default setup uses a smaller font within
+ proofs.
\medskip The $text$ part of each of the various markup commands
- considered so far essentially inserts quoted material within a
- formal text, mainly for instruction of the reader (arbitrary
- {\LaTeX} macros may be also included). An \bfindex{antiquotation}
- is again a formal object that has been embedded into such an
- informal portion. The interpretation of antiquotations is limited
- to some well-formedness checks, with the result being pretty printed
- to the resulting document. So quoted text blocks together with
- antiquotations provide very handsome means to reference formal
- entities with good confidence in technical details (especially
- syntax and types).
+ considered so far essentially inserts \emph{quoted material} into a
+ formal text, mainly for instruction of the reader. An
+ \bfindex{antiquotation} is again a formal object embedded into such
+ an informal portion. The interpretation of antiquotations is
+ limited to some well-formedness checks, with the result being pretty
+ printed to the resulting document. So quoted text blocks together
+ with antiquotations provide very handsome means to reference formal
+ entities with good confidence in getting the technical details right
+ (especially syntax and types).
The general syntax of antiquotations is as follows:
\texttt{{\at}{\ttlbrace}$name$ $arguments${\ttrbrace}}, or
\texttt{{\at}{\ttlbrace}$name$ [$options$] $arguments${\ttrbrace}}
for a comma-separated list of options consisting of a $name$ or
- \texttt{$name$=$value$} pair \cite{isabelle-isar-ref}. The syntax
- of $arguments$ depends on the kind of antiquotation, it generally
- follows the same conventions for types, terms, or theorems as in the
- formal part of a theory.
+ \texttt{$name$=$value$}. The syntax of $arguments$ depends on the
+ kind of antiquotation, it generally follows the same conventions for
+ types, terms, or theorems as in the formal part of a theory.
\medskip Here is an example of the quotation-antiquotation
technique: \isa{{\isasymlambda}x\ y{\isachardot}\ x} is a well-typed term.
@@ -620,20 +618,20 @@
From the notational change of the ASCII character \verb,%, to the
symbol \isa{{\isasymlambda}} we see that the term really got printed by the
- system (after parsing and type-checking), document preparation
+ system (after parsing and type-checking) --- document preparation
enables symbolic output by default.
\medskip The next example includes an option to modify the
\verb,show_types, flag of Isabelle:
- \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces \isa{{\isasymlambda}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ y{\isasymColon}{\isacharprime}b{\isachardot}\ x}. Here type-inference has figured out the
- most general typings in the present (theory) context. Note that
- term fragments may acquire a different typings due to constraints
- imposed by previous text (within a proof), say by the main goal
- statement given before hand.
+ \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
+ general typings in the present (theory) context. Note that term
+ fragments may acquire different typings due to constraints imposed
+ by previous text (say within a proof), e.g.\ due to the main goal
+ statement given beforehand.
\medskip Several further kinds of antiquotations (and options) are
available \cite{isabelle-sys}. Here are a few commonly used
- combinations are as follows:
+ combinations:
\medskip
@@ -676,45 +674,47 @@
%
\begin{isamarkuptext}%
As has been pointed out before (\S\ref{sec:syntax-symbols}),
- Isabelle symbols are the the smallest syntactic entities, a
+ Isabelle symbols are the smallest syntactic entities --- a
straight-forward generalization of ASCII characters. While Isabelle
does not impose any interpretation of the infinite collection of
- symbols, the {\LaTeX} document output produces the canonical output
- for certain standard symbols \cite[appendix~A]{isabelle-sys}.
+ named symbols, {\LaTeX} documents show canonical glyphs for certain
+ standard symbols \cite[appendix~A]{isabelle-sys}.
The {\LaTeX} code produced from Isabelle text follows a relatively
- simple scheme (see below). Users may wish to tune the final
- appearance by redefining certain macros, say in \texttt{root.tex} of
- the document.
+ simple scheme. Users may wish to tune the final appearance by
+ redefining certain macros, say in \texttt{root.tex} of the document.
+
+ \begin{enumerate}
- \begin{enumerate} \item 7-bit ASCII characters: letters
- \texttt{A\dots Z} and \texttt{a\dots z} are output verbatim, digits
- are passed as an argument to the \verb,\isadigit, macro, other
- characters are replaced by specifically named macros of the form
+ \item 7-bit ASCII characters: letters \texttt{A\dots Z} and
+ \texttt{a\dots z} are output verbatim, digits are passed as an
+ argument to the \verb,\isadigit, macro, other characters are
+ replaced by specifically named macros of the form
\verb,\isacharXYZ,.
\item Named symbols: \verb,\,\verb,<,$XYZ$\verb,>, become
- \verb,{\isasym,$XYZ$\verb,}, each (note the additional braces). See
- \cite[appendix~A]{isabelle-sys} and \texttt{isabellesym.sty} for the
- collection of predefined standard symbols.
+ \verb,{\isasym,$XYZ$\verb,}, each (note the additional braces).
- \item Named control symbols: \verb,\,\verb,<^,$XYZ$\verb,>, become
- \verb,\isactrl,$XYZ$; subsequent symbols may act as arguments, if
- the corresponding macro is defined accordingly.
+ \item Named control symbols: \verb,{\isasym,$XYZ$\verb,}, become
+ \verb,\isactrl,$XYZ$ each; subsequent symbols may act as arguments
+ if the corresponding macro is defined accordingly.
+
\end{enumerate}
- Users may occasionally wish to invent new named symbols; this merely
- requires an appropriate definition of \verb,\,\verb,<,$XYZ$\verb,>,
- as far as {\LaTeX} output is concerned. Control symbols are
- slightly more difficult to get right, though.
+ Users may occasionally wish to give new {\LaTeX} interpretations of
+ named symbols; this merely requires an appropriate definition of
+ \verb,\,\verb,<,$XYZ$\verb,>, (see \texttt{isabelle.sty} for working
+ examples). Control symbols are slightly more difficult to get
+ right, though.
\medskip The \verb,\isabellestyle, macro provides a high-level
interface to tune the general appearance of individual symbols. For
- example, \verb,\isabellestyle{it}, uses italics fonts to mimic the
- general appearance of the {\LaTeX} math mode; double quotes are not
- printed at all. The resulting quality of type-setting is quite
- good, so this should probably be the default style for real
- production work that gets distributed to a broader audience.%
+ example, \verb,\isabellestyle{it}, uses the italics text style to
+ mimic the general appearance of the {\LaTeX} math mode; double
+ quotes are not printed at all. The resulting quality of
+ type-setting is quite good, so this should usually be the default
+ style for real production work that gets distributed to a broader
+ audience.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -723,36 +723,35 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-By default Isabelle's document system generates a {\LaTeX} source
- file for each theory that happens to get loaded during the session.
- The generated \texttt{session.tex} will include all of these in
- order of appearance, which in turn gets included by the standard
- \texttt{root.tex}. Certainly one may change the order of appearance
- or suppress unwanted theories by ignoring \texttt{session.tex} and
+By default, Isabelle's document system generates a {\LaTeX} source
+ file for each theory that happens to get loaded while running the
+ session. The generated \texttt{session.tex} will include all of
+ these in order of appearance, which in turn gets included by the
+ standard \texttt{root.tex}. Certainly one may change the order or
+ suppress unwanted theories by ignoring \texttt{session.tex} and
include individual files in \texttt{root.tex} by hand. On the other
hand, such an arrangement requires additional maintenance chores
whenever the collection of theories changes.
Alternatively, one may tune the theory loading process in
\texttt{ROOT.ML} itself: traversal of the theory dependency graph
- may be fine-tuned by adding further \verb,use_thy, invocations,
- although topological sorting still has to be observed. Moreover,
- the ML operator \verb,no_document, temporarily disables document
- generation while executing a theory loader command; its usage is
- like this:
+ may be fine-tuned by adding \verb,use_thy, invocations, although
+ topological sorting still has to be observed. Moreover, the ML
+ operator \verb,no_document, temporarily disables document generation
+ while executing a theory loader command; its usage is like this:
\begin{verbatim}
no_document use_thy "T";
\end{verbatim}
- \medskip Theory output may be also suppressed in smaller portions as
- well. For example, research papers or slides usually do not include
- the formal content in full. In order to delimit \bfindex{ignored
+ \medskip Theory output may be also suppressed in smaller portions.
+ For example, research articles, or slides usually do not include the
+ formal content in full. In order to delimit \bfindex{ignored
material} special source comments
\verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
\verb,(,\verb,*,\verb,>,\verb,*,\verb,), may be included in the
text. Only the document preparation system is affected, the formal
- checking the theory is performed as before.
+ checking the theory is performed unchanged.
In the following example we suppress the slightly formalistic
\isakeyword{theory} + \isakeyword{end} surroundings a theory.
@@ -771,10 +770,10 @@
\medskip
- Text may be suppressed in a fine grained manner. For example, we
- may even drop vital parts of a formal proof, pretending that things
- have been simpler than in reality. For example, the following
- ``fully automatic'' proof is actually a fake:%
+ Text may be suppressed in a fine grained manner. We may even drop
+ vital parts of a formal proof, pretending that things have been
+ simpler than in reality. For example, the following ``fully
+ automatic'' proof is actually a fake:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ {\isachardoublequote}x\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isacharless}\ x\ {\isacharasterisk}\ x{\isachardoublequote}\isanewline
@@ -790,26 +789,26 @@
%(*
\medskip Ignoring portions of printed does demand some care by the
- user. First of all, the writer is responsible not to obfuscate the
- underlying formal development in an unduly manner. It is fairly
+ writer. First of all, the writer is responsible not to obfuscate
+ the underlying formal development in an unduly manner. It is fairly
easy to invalidate the remaining visible text, e.g.\ by referencing
questionable formal items (strange definitions, arbitrary axioms
etc.) that have been hidden from sight beforehand.
- Some minor technical subtleties of the
+ Authentic reports of formal theories, say as part of a library,
+ usually should refrain from suppressing parts of the text at all.
+ Other users may need the full information for their own derivative
+ work. If a particular formalization appears inadequate for general
+ public coverage, it is often more appropriate to think of a better
+ way in the first place.
+
+ \medskip Some technical subtleties of the
\verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
- elements need to be kept in mind as well, since the system performs
- little sanity checks here. Arguments of markup commands and formal
+ elements need to be kept in mind, too --- the system performs little
+ sanity checks here. Arguments of markup commands and formal
comments must not be hidden, otherwise presentation fails. Open and
close parentheses need to be inserted carefully; it is fairly easy
- to hide the wrong parts, especially after rearranging the sources.
-
- \medskip Authentic reports of formal theories, say as part of a
- library, usually should refrain from suppressing parts of the text
- at all. Other users may need the full information for their own
- derivative work. If a particular formalization appears inadequate
- for general public coverage, it is often more appropriate to think
- of a better way in the first place.%
+ to hide the wrong parts, especially after rearranging the sources.%
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%