--- a/doc-src/TutorialI/Documents/Documents.thy Tue Jan 15 15:07:41 2002 +0100
+++ b/doc-src/TutorialI/Documents/Documents.thy Tue Jan 15 17:54:28 2002 +0100
@@ -5,18 +5,16 @@
section {* Concrete Syntax \label{sec:concrete-syntax} *}
text {*
- The core concept of Isabelle's framework for concrete
- syntax is that of \bfindex{mixfix annotations}. Associated
- with any kind of constant declaration, mixfixes affect both the
- grammar productions for the parser and output templates for the
- pretty printer.
+ The core concept of Isabelle's framework for concrete syntax is that
+ of \bfindex{mixfix annotations}. Associated with any kind of
+ constant declaration, mixfixes affect both the grammar productions
+ for the parser and output templates for the pretty printer.
In full generality, parser and pretty printer configuration is a
- subtle affair \cite{isabelle-ref}. Your syntax
- specifications need to interact properly with the
- existing setup of Isabelle/Pure and Isabelle/HOL\@.
- To avoid creating ambiguities with existing elements, it is
- particularly important to give new syntactic
+ subtle affair \cite{isabelle-ref}. Your syntax specifications need
+ to interact properly with the existing setup of Isabelle/Pure and
+ Isabelle/HOL\@. To avoid creating ambiguities with existing
+ elements, it is particularly important to give new syntactic
constructs the right precedence.
\medskip Subsequently we introduce a few simple syntax declaration
@@ -28,16 +26,15 @@
text {*
Syntax annotations may be included wherever constants are declared,
- such as \isacommand{consts} and
- \isacommand{constdefs} --- and also \isacommand{datatype}, which
- declares constructor operations. Type-constructors may be annotated as
- well, although this is less frequently encountered in practice (the
- infix type @{text "\<times>"} comes to mind).
+ such as \isacommand{consts} and \isacommand{constdefs} --- and also
+ \isacommand{datatype}, which declares constructor operations.
+ Type-constructors may be annotated as well, although this is less
+ frequently encountered in practice (the infix type @{text "\<times>"} comes
+ to mind).
Infix declarations\index{infix annotations} provide a useful special
- case of mixfixes. The following example of the
- exclusive-or operation on boolean values illustrates typical infix
- declarations.
+ case of mixfixes. The following example of the exclusive-or
+ operation on boolean values illustrates typical infix declarations.
*}
constdefs
@@ -47,53 +44,51 @@
text {*
\noindent Now @{text "xor A B"} and @{text "A [+] B"} refer to the
same expression internally. Any curried function with at least two
- arguments may be given infix syntax. For partial
- applications with fewer than two operands, there is a notation
- using the prefix~\isa{op}. For instance, @{text xor} without arguments is represented
- as @{text "op [+]"}; together with ordinary function application, this
+ arguments may be given infix syntax. For partial applications with
+ fewer than two operands, there is a notation using the prefix~@{text
+ op}. For instance, @{text xor} without arguments is represented as
+ @{text "op [+]"}; together with ordinary function application, this
turns @{text "xor A"} into @{text "op [+] A"}.
\medskip The keyword \isakeyword{infixl} seen above specifies an
infix operator that is nested to the \emph{left}: in iterated
applications the more complex expression appears on the left-hand
- side, and @{term "A [+] B [+] C"} stands for @{text "(A [+] B) [+] C"}.
- Similarly, \isakeyword{infixr} specifies nesting to the
+ side, and @{term "A [+] B [+] C"} stands for @{text "(A [+] B) [+]
+ C"}. Similarly, \isakeyword{infixr} means nesting to the
\emph{right}, reading @{term "A [+] B [+] C"} as @{text "A [+] (B
- [+] C)"}. In contrast, a \emph{non-oriented} declaration via
- \isakeyword{infix} would render @{term "A [+] B [+] C"} illegal, but
- demand explicit parentheses to indicate the intended grouping.
+ [+] C)"}. A \emph{non-oriented} declaration via \isakeyword{infix}
+ would render @{term "A [+] B [+] C"} illegal, but demand explicit
+ parentheses to indicate the intended grouping.
The string @{text [source] "[+]"} in our annotation refers to the
concrete syntax to represent the operator (a literal token), while
the number @{text 60} determines the precedence of the construct:
- the syntactic priorities of the arguments and result.
- Isabelle/HOL already uses up many popular combinations of
- ASCII symbols for its own use, including both @{text "+"} and @{text
- "++"}. Longer character combinations are
- more likely to be still available for user extensions, such as our~@{text "[+]"}.
+ the syntactic priorities of the arguments and result. Isabelle/HOL
+ already uses up many popular combinations of ASCII symbols for its
+ own use, including both @{text "+"} and @{text "++"}. Longer
+ character combinations are more likely to be still available for
+ user extensions, such as our~@{text "[+]"}.
- Operator precedences have a range of 0--1000. Very low or high priorities are
- reserved for the meta-logic. HOL syntax
- mainly uses the range of 10--100: the equality infix @{text "="} is
- centered at 50; logical connectives (like @{text "\<or>"} and @{text
- "\<and>"}) are below 50; algebraic ones (like @{text "+"} and @{text
- "*"}) are above 50. User syntax should strive to coexist with common
- HOL forms, or use the mostly unused range 100--900.
-
+ Operator precedences have a range of 0--1000. Very low or high
+ priorities are reserved for the meta-logic. HOL syntax mainly uses
+ the range of 10--100: the equality infix @{text "="} is centered at
+ 50; logical connectives (like @{text "\<or>"} and @{text "\<and>"}) are
+ below 50; algebraic ones (like @{text "+"} and @{text "*"}) are
+ above 50. User syntax should strive to coexist with common HOL
+ forms, or use the mostly unused range 100--900.
*}
subsection {* Mathematical Symbols \label{sec:syntax-symbols} *}
text {*
- Concrete syntax based on ASCII characters has inherent
- limitations. Mathematical notation demands a larger repertoire
- 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
- encodings. There are three kinds of such ``generalized
- characters'':
+ Concrete syntax based on ASCII characters has inherent limitations.
+ Mathematical notation demands a larger repertoire of glyphs.
+ Several standards of extended character sets have been proposed over
+ decades, but none has become universally available so far. Isabelle
+ has its own notion of \bfindex{symbols} as the smallest entities of
+ source text, without referring to internal encodings. There are
+ three kinds of such ``generalized characters'':
\begin{enumerate}
@@ -107,13 +102,13 @@
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 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 as~@{text \<forall>}.
+ interpretation is left to further front-end tools. For example, 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 as~@{text \<forall>}.
A list of standard Isabelle symbols is given in
- \cite[appendix~A]{isabelle-sys}. You may introduce their own
+ \cite[appendix~A]{isabelle-sys}. You may introduce your own
interpretation of further symbols by configuring the appropriate
front-end tool accordingly, e.g.\ by defining certain {\LaTeX}
macros (see also \S\ref{sec:doc-prep-symbols}). There are also a
@@ -122,7 +117,7 @@
printable symbol, respectively. For example, \verb,A\<^sup>\<star>, is
output as @{text "A\<^sup>\<star>"}.
- \medskip Replacing our definition of @{text xor} by the following
+ \medskip Replacing our definition of @{text xor} by the following
specifies a Isabelle symbol for the new operator:
*}
@@ -140,15 +135,14 @@
text {*
\noindent The X-Symbol package within Proof~General provides several
input methods to enter @{text \<oplus>} in the text. If all fails one may
- just type a named entity \verb,\,\verb,<oplus>, by hand; the
- corresponding symbol will immediately be displayed.
+ just type a named entity \verb,\,\verb,<oplus>, by hand; the
+ corresponding symbol will be displayed after further input.
- \medskip More flexible is to provide alternative
- syntax forms through the \bfindex{print mode} concept~\cite{isabelle-ref}.
- By convention, the mode of
- ``$xsymbols$'' is enabled whenever Proof~General's X-Symbol mode or
- {\LaTeX} output is active. Now consider the following hybrid
- declaration of @{text xor}:
+ \medskip More flexible is to provide alternative syntax forms
+ through the \bfindex{print mode} concept~\cite{isabelle-ref}. By
+ convention, the mode of ``$xsymbols$'' is enabled whenever
+ Proof~General's X-Symbol mode or {\LaTeX} output is active. Now
+ consider the following hybrid declaration of @{text xor}:
*}
(*<*)
@@ -174,21 +168,20 @@
with the real constant.
\medskip We may now write @{text "A [+] B"} or @{text "A \<oplus> B"} in
- input, while output uses the nicer syntax of $xsymbols$, provided
+ input, while output uses the nicer syntax of $xsymbols$ whenever
that print mode is active. Such an arrangement is particularly
- useful for interactive development, where users may type ASCII
- text and see mathematical symbols displayed during proofs.
+ useful for interactive development, where users may type ASCII text
+ and see mathematical symbols displayed during proofs.
*}
subsection {* Prefix Annotations *}
text {*
- Prefix syntax annotations\index{prefix annotation} are another
- 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.
+ Prefix syntax annotations\index{prefix annotation} are another form
+ of mixfixes \cite{isabelle-ref}, without any template arguments or
+ priorities --- just some literal syntax. The following example
+ associates common symbols with the constructors of a datatype.
*}
datatype currency =
@@ -208,7 +201,7 @@
achieves conformance with notational standards of the European
Commission.
- Prefix syntax also works for \isakeyword{consts} or
+ Prefix syntax works the same way for \isakeyword{consts} or
\isakeyword{constdefs}.
*}
@@ -216,22 +209,22 @@
subsection {* Syntax Translations \label{sec:syntax-translations} *}
text{*
- Mixfix syntax annotations merely decorate
- particular constant application forms with
- concrete syntax, for instance replacing \ @{text "xor A B"} by @{text "A \<oplus> B"}. Occasionally, the relationship between some piece of
- notation and its internal form is more complicated. Here we need
- \bfindex{syntax translations}.
+ Mixfix syntax annotations merely decorate particular constant
+ application forms with concrete syntax, for instance replacing \
+ @{text "xor A B"} by @{text "A \<oplus> B"}. Occasionally, the
+ relationship between some piece of notation and its internal form is
+ more complicated. Here we need \bfindex{syntax translations}.
Using the \isakeyword{syntax}\index{syntax (command)}, command we
introduce uninterpreted notational elements. Then
\commdx{translations} relate input forms to complex logical
- expressions. This provides a simple mechanism for
- syntactic macros; even heavier transformations may be written in ML
+ expressions. This provides a simple mechanism for syntactic macros;
+ even heavier transformations may be written in ML
\cite{isabelle-ref}.
\medskip A typical use of syntax translations is to introduce
- relational notation for membership in a set of pair,
- replacing \ @{text "(x, y) \<in> sim"} by @{text "x \<approx> y"}.
+ relational notation for membership in a set of pair, replacing \
+ @{text "(x, y) \<in> sim"} by @{text "x \<approx> y"}.
*}
consts
@@ -244,8 +237,8 @@
text {*
\noindent Here the name of the dummy constant @{text "_sim"} does
- not matter, as long as it is not used elsewhere. Prefixing
- an underscore is a common convention. The \isakeyword{translations}
+ not matter, as long as it is not used elsewhere. Prefixing an
+ underscore is a common convention. The \isakeyword{translations}
declaration already uses concrete syntax on the left-hand side;
internally we relate a raw application @{text "_sim x y"} with
@{text "(x, y) \<in> sim"}.
@@ -267,11 +260,10 @@
replaced by the ``definition'' upon parsing; the effect is reversed
upon printing.
- This sort of translation is appropriate when the
- defined concept is a trivial variation on an
- existing one. On the other hand, syntax translations do not scale
- up well to large hierarchies of concepts. Translations
- do not replace definitions!
+ This sort of translation is appropriate when the defined concept is
+ a trivial variation on an existing one. On the other hand, syntax
+ translations do not scale up well to large hierarchies of concepts.
+ Translations do not replace definitions!
*}
@@ -279,19 +271,18 @@
text {*
Isabelle/Isar is centered around the concept of \bfindex{formal
- proof documents}\index{documents|bold}. The outcome of a
- formal development effort is meant to be a human-readable record,
- presented as browsable PDF file or printed on paper. The overall
- document structure follows traditional mathematical articles, with
- sections, intermediate explanations, definitions, theorems and
- proofs.
+ proof documents}\index{documents|bold}. The outcome of a formal
+ development effort is meant to be a human-readable record, presented
+ as browsable PDF file or printed on paper. The overall document
+ structure follows traditional mathematical articles, with sections,
+ intermediate explanations, definitions, theorems and proofs.
\medskip The Isabelle document preparation system essentially acts
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 lets you write
- authentic reports on theory developments with little effort: many
- technical consistency checks are handled by the system.
+ instructions in a schematic manner. This lets you write authentic
+ reports on theory developments with little effort: many technical
+ consistency checks are handled by the system.
Here is an example to illustrate the idea of Isabelle document
preparation.
@@ -316,8 +307,7 @@
text_raw {* \end{quotation} *}
text {*
- The above document output has been produced by the following theory
- specification:
+ \noindent The above document output has been produced as follows:
\begin{ttbox}
text {\ttlbrace}*
@@ -328,16 +318,17 @@
datatype 'a bintree =
Leaf | Branch 'a "'a bintree" "'a bintree"
-
+ \end{ttbox}
+ \begin{ttbox}
text {\ttlbrace}*
{\ttback}noindent The datatype induction rule generated here is
of the form {\at}{\ttlbrace}thm [display] bintree.induct [no_vars]{\ttrbrace}
*{\ttrbrace}
- \end{ttbox}
+ \end{ttbox}\vspace{-\medskipamount}
\noindent Here we have augmented the theory by formal comments
- (using \isakeyword{text} blocks). The informal parts may again
- refer to formal entities by means of ``antiquotations'' (such as
+ (using \isakeyword{text} blocks), the informal parts may again refer
+ to formal entities by means of ``antiquotations'' (such as
\texttt{\at}\verb,{text "'a bintree"}, or
\texttt{\at}\verb,{typ 'a},), see also \S\ref{sec:doc-prep-text}.
*}
@@ -349,11 +340,11 @@
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} consists of a collection
- of source files that may contribute to an output document.
- Each session is derived from a single parent, 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,).
+ of source files that may contribute to an output document. Each
+ session is derived from a single parent, 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,).
\medskip The easiest way to manage Isabelle sessions is via
\texttt{isatool mkdir} (generates an initial session source setup)
@@ -372,7 +363,7 @@
to produce some \texttt{document.pdf} (with dummy title, empty table
of contents etc.). Any failure at this stage usually indicates
technical problems of the {\LaTeX} installation.\footnote{Especially
- make sure that \texttt{pdflatex} is present; if all fails one may
+ make sure that \texttt{pdflatex} is present; if in doubt one may
fall back on DVI output by changing \texttt{usedir} options in
\texttt{IsaMakefile} \cite{isabelle-sys}.}
@@ -411,8 +402,8 @@
\end{itemize}
One may now start to populate the directory \texttt{MySession}, and
- the file \texttt{MySession/ROOT.ML} accordingly.
- The file \texttt{MySession/document/root.tex} should also be adapted at some
+ the file \texttt{MySession/ROOT.ML} accordingly. The file
+ \texttt{MySession/document/root.tex} should also be adapted at some
point; the default version is mostly self-explanatory. Note that
\verb,\isabellestyle, enables fine-tuning of the general appearance
of characters and mathematical symbols (see also
@@ -427,15 +418,14 @@
\medskip Any additional files for the {\LaTeX} stage go into the
\texttt{MySession/document} directory as well. In particular,
- adding a file named \texttt{root.bib} causes an
- automatic run of \texttt{bibtex} to process a bibliographic
- database; see also \texttt{isatool document} \cite{isabelle-sys}.
+ adding a file named \texttt{root.bib} causes an automatic run of
+ \texttt{bibtex} to process a bibliographic database; see also
+ \texttt{isatool document} \cite{isabelle-sys}.
\medskip Any failure of the document preparation phase in an
Isabelle batch session leaves the generated sources in their target
- location, identified by the accompanying error message. This
- lets you trace {\LaTeX} problems with the generated files at
- hand.
+ location, identified by the accompanying error message. This lets
+ you trace {\LaTeX} problems with the generated files at hand.
*}
@@ -470,9 +460,9 @@
$text$ argument (delimited by \verb,",~@{text \<dots>}~\verb,", or
\verb,{,\verb,*,~@{text \<dots>}~\verb,*,\verb,},). After stripping any
surrounding white space, the argument is passed to a {\LaTeX} macro
- \verb,\isamarkupXYZ, for any command \isakeyword{XYZ}. These macros
- are defined in \verb,isabelle.sty, according to the meaning given in
- the rightmost column above.
+ \verb,\isamarkupXYZ, for command \isakeyword{XYZ}. These macros are
+ defined in \verb,isabelle.sty, according to the meaning given in the
+ rightmost column above.
\medskip The following source fragment illustrates structure markup
of a theory. Note that {\LaTeX} labels may be included inside of
@@ -501,22 +491,20 @@
theorem main: \dots
end
- \end{ttbox}
+ \end{ttbox}\vspace{-\medskipamount}
- You may occasionally want to change the meaning of markup
- commands, say via \verb,\renewcommand, in \texttt{root.tex}. For example,
- \verb,\isamarkupheader, is a good candidate for some tuning.
- We could
- move it up in the hierarchy to become \verb,\chapter,.
+ You may occasionally want to change the meaning of markup commands,
+ say via \verb,\renewcommand, in \texttt{root.tex}. For example,
+ \verb,\isamarkupheader, is a good candidate for some tuning. We
+ could move it up in the hierarchy to become \verb,\chapter,.
\begin{verbatim}
\renewcommand{\isamarkupheader}[1]{\chapter{#1}}
\end{verbatim}
- \noindent Now we must change the
- document class given in \texttt{root.tex} to something that supports
- chapters. A suitable command is
- \verb,\documentclass{report},.
+ \noindent Now we must change the document class given in
+ \texttt{root.tex} to something that supports chapters. A suitable
+ command is \verb,\documentclass{report},.
\medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
hold the name of the current theory context. This is particularly
@@ -587,27 +575,27 @@
\renewcommand{\isastyletxt}{\isastyletext}
\end{verbatim}
- \medskip The $text$ part of these markup commands
- 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. Quoted text blocks together with
- antiquotations provide an attractive means of referring to formal
- entities, with good confidence in getting the technical details
- right (especially syntax and types).
+ \medskip The $text$ part of Isabelle markup commands 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. Quoted text blocks together with antiquotations provide
+ an attractive means of referring to 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$}. 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$} each. 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 This sentence demonstrates quotations and antiquotations:
- @{term "%x y. x"} is a well-typed term.
+ \medskip This sentence demonstrates quotations and antiquotations:
+ @{term "%x y. x"} is a well-typed term.
\medskip\noindent The output above was produced as follows:
\begin{ttbox}
@@ -615,22 +603,21 @@
This sentence demonstrates quotations and antiquotations:
{\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term.
*{\ttrbrace}
- \end{ttbox}
+ \end{ttbox}\vspace{-\medskipamount}
The notational change from the ASCII character~\verb,%, to the
- symbol~@{text \<lambda>} reveals that Isabelle printed this term,
- after parsing and type-checking. Document preparation
- enables symbolic output by default.
+ symbol~@{text \<lambda>} reveals that Isabelle printed this term, after
+ parsing and type-checking. Document preparation enables symbolic
+ output by default.
\medskip The next example includes an option to modify Isabelle's
\verb,show_types, flag. The antiquotation
- \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces
- the output @{term [show_types] "%x y. x"}.
- Type inference has figured out the most
- general typings in the present theory context. Terms
- may acquire different typings due to constraints imposed
- by their environment; within a proof, for example, variables are given
- the same types as they have in the main goal statement.
+ \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces the
+ output @{term [show_types] "%x y. x"}. Type inference has figured
+ out the most general typings in the present theory context. Terms
+ may acquire different typings due to constraints imposed by their
+ environment; within a proof, for example, variables are given the
+ same types as they have in the main goal statement.
\medskip Several further kinds of antiquotations and options are
available \cite{isabelle-sys}. Here are a few commonly used
@@ -667,8 +654,9 @@
"\<forall>\<exists>"}, according to the standard interpretation of these symbol
(cf.\ \S\ref{sec:doc-prep-symbols}). Thus we achieve consistent
mathematical notation in both the formal and informal parts of the
- document very easily. Manual {\LaTeX} code would leave more control
- over the typesetting, but is also slightly more tedious.
+ document very easily, independently of the term language of
+ Isabelle. Manual {\LaTeX} code would leave more control over the
+ typesetting, but is also slightly more tedious.
*}
@@ -682,9 +670,9 @@
named symbols, {\LaTeX} documents use canonical glyphs for certain
standard symbols \cite[appendix~A]{isabelle-sys}.
- The {\LaTeX} code produced from Isabelle text follows a
- simple scheme. You can tune the final appearance by
- redefining certain macros, say in \texttt{root.tex} of the document.
+ The {\LaTeX} code produced from Isabelle text follows a simple
+ scheme. You can tune the final appearance by redefining certain
+ macros, say in \texttt{root.tex} of the document.
\begin{enumerate}
@@ -694,18 +682,18 @@
replaced by specifically named macros of the form
\verb,\isacharXYZ,.
- \item Named symbols: \verb,\,\verb,<,$XYZ$\verb,>, is turned into
- \verb,{\isasym,$XYZ$\verb,},; note the additional braces.
+ \item Named symbols: \verb,\,\verb,<XYZ>, is turned into
+ \verb,{\isasymXYZ},; note the additional braces.
- \item Named control symbols: \verb,\,\verb,<^,$XYZ$\verb,>, is
- turned into \verb,\isactrl,$XYZ$; subsequent symbols may act as
- arguments if the corresponding macro is defined accordingly.
+ \item Named control symbols: \verb,\,\verb,<^XYZ>, is turned into
+ \verb,\isactrlXYZ,; subsequent symbols may act as arguments if the
+ control macro is defined accordingly.
\end{enumerate}
You may occasionally wish to give new {\LaTeX} interpretations of
named symbols. This merely requires an appropriate definition of
- \verb,\isasym,$XYZ$\verb,, for \verb,\,\verb,<,$XYZ$\verb,>, (see
+ \verb,\isasymXYZ,, for \verb,\,\verb,<XYZ>, (see
\texttt{isabelle.sty} for working examples). Control symbols are
slightly more difficult to get right, though.
@@ -737,23 +725,22 @@
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:
+ 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 suppressed more selectively.
- Research articles and 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 document preparation is affected; the formal
- checking of the theory is unchanged.
+ \medskip Theory output may be suppressed more selectively. Research
+ articles and slides usually do not include the formal content in
+ full. Delimiting \bfindex{ignored material} by the special source
+ comments \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
+ \verb,(,\verb,*,\verb,>,\verb,*,\verb,), tells the document
+ preparation system to suppress these parts; the formal checking of
+ the theory is unchanged.
- In this example, we suppress a theory's uninteresting
- \isakeyword{theory} and \isakeyword{end} brackets:
+ In this example, we hide a theory's \isakeyword{theory} and
+ \isakeyword{end} brackets:
\medskip
@@ -771,8 +758,8 @@
Text may be suppressed in a fine-grained manner. We may even hide
vital parts of a proof, pretending that things have been simpler
- than they really were. For example, this ``fully automatic'' proof is
- actually a fake:
+ than they really were. For example, this ``fully automatic'' proof
+ is actually a fake:
*}
lemma "x \<noteq> (0::int) \<Longrightarrow> 0 < x * x"
@@ -786,18 +773,16 @@
\end{verbatim}
%(*
- \medskip Suppressing portions of printed text demands care.
- You should not misrepresent
- the underlying theory development. It is
- easy to invalidate the visible text by hiding
- references to questionable axioms.
+ \medskip Suppressing portions of printed text demands care. You
+ should not misrepresent the underlying theory development. It is
+ easy to invalidate the visible text by hiding references to
+ questionable axioms.
Authentic reports of Isabelle/Isar theories, say as part of a
- library, should suppress nothing.
- 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.
+ library, should suppress nothing. 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,),