diff -r 7d67b065925e -r 072e9d582db0 doc-src/TutorialI/Documents/document/Documents.tex --- a/doc-src/TutorialI/Documents/document/Documents.tex Tue Jan 15 17:54:28 2002 +0100 +++ b/doc-src/TutorialI/Documents/document/Documents.tex Tue Jan 15 17:54:31 2002 +0100 @@ -8,18 +8,16 @@ \isamarkuptrue% % \begin{isamarkuptext}% -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 @@ -33,16 +31,15 @@ % \begin{isamarkuptext}% 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 \isa{{\isasymtimes}} 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 \isa{{\isasymtimes}} 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.% \end{isamarkuptext}% \isamarkuptrue% \isacommand{constdefs}\isanewline @@ -52,34 +49,35 @@ \begin{isamarkuptext}% \noindent Now \isa{xor\ A\ B} and \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ 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, \isa{xor} without arguments is represented - as \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}}; 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~\isa{op}. For instance, \isa{xor} without arguments is represented as + \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}}; together with ordinary function application, this turns \isa{xor\ A} into \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ 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 \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 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 render \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but - demand explicit parentheses to indicate the intended grouping. + 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}. Similarly, \isakeyword{infixr} means 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}}. A \emph{non-oriented} declaration via \isakeyword{infix} + would render \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but demand explicit + parentheses to indicate the intended grouping. The string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in our annotation refers to the concrete syntax to represent the operator (a literal token), while the number \isa{{\isadigit{6}}{\isadigit{0}}} 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 \isa{{\isacharplus}} and \isa{{\isacharplus}{\isacharplus}}. Longer character combinations are - more likely to be still available for user extensions, such as our~\isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}}. + 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 \isa{{\isacharplus}} and \isa{{\isacharplus}{\isacharplus}}. Longer + character combinations are more likely to be still available for + user extensions, such as our~\isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}}. - 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 \isa{{\isacharequal}} is - 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 - 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 \isa{{\isacharequal}} is 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 HOL + forms, or use the mostly unused range 100--900.% \end{isamarkuptext}% \isamarkuptrue% % @@ -88,14 +86,13 @@ \isamarkuptrue% % \begin{isamarkuptext}% -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} @@ -109,13 +106,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,, symbol as~\isa{{\isasymforall}}. + 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,, symbol as~\isa{{\isasymforall}}. 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 @@ -124,7 +121,7 @@ printable symbol, respectively. For example, \verb,A\<^sup>\, is output as \isa{A\isactrlsup {\isasymstar}}. - \medskip Replacing our definition of \isa{xor} by the following + \medskip Replacing our definition of \isa{xor} by the following specifies a Isabelle symbol for the new operator:% \end{isamarkuptext}% \isamarkuptrue% @@ -138,15 +135,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 a named entity \verb,\,\verb,, by hand; the - corresponding symbol will immediately be displayed. + just type a named entity \verb,\,\verb,, 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 \isa{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 \isa{xor}:% \end{isamarkuptext}% \isamarkuptrue% \isamarkupfalse% @@ -168,10 +164,10 @@ with the real constant. \medskip We may now write \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} or \isa{A\ {\isasymoplus}\ 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.% \end{isamarkuptext}% \isamarkuptrue% % @@ -180,11 +176,10 @@ \isamarkuptrue% % \begin{isamarkuptext}% -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.% \end{isamarkuptext}% \isamarkuptrue% \isacommand{datatype}\ currency\ {\isacharequal}\isanewline @@ -203,7 +198,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}.% \end{isamarkuptext}% \isamarkuptrue% @@ -213,22 +208,22 @@ \isamarkuptrue% % \begin{isamarkuptext}% -Mixfix syntax annotations merely decorate - particular constant application forms with - concrete syntax, for instance replacing \ \isa{xor\ A\ B} by \isa{A\ {\isasymoplus}\ 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 \ + \isa{xor\ A\ B} by \isa{A\ {\isasymoplus}\ 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 \ \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} by \isa{x\ {\isasymapprox}\ y}.% + relational notation for membership in a set of pair, replacing \ + \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} by \isa{x\ {\isasymapprox}\ y}.% \end{isamarkuptext}% \isamarkuptrue% \isacommand{consts}\isanewline @@ -243,8 +238,8 @@ % \begin{isamarkuptext}% \noindent Here the name of the dummy constant \isa{{\isacharunderscore}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 \isa{{\isacharunderscore}sim\ x\ y} with \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim}. @@ -267,11 +262,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!% \end{isamarkuptext}% \isamarkuptrue% % @@ -281,19 +275,18 @@ % \begin{isamarkuptext}% 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.% @@ -324,8 +317,7 @@ \end{quotation} % \begin{isamarkuptext}% -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}* @@ -336,16 +328,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}.% \end{isamarkuptext}% @@ -359,11 +352,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) @@ -382,7 +375,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}.} @@ -421,8 +414,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 @@ -437,15 +430,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.% \end{isamarkuptext}% \isamarkuptrue% % @@ -482,9 +474,9 @@ $text$ argument (delimited by \verb,",~\isa{{\isasymdots}}~\verb,", or \verb,{,\verb,*,~\isa{{\isasymdots}}~\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 @@ -513,22 +505,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 @@ -611,27 +601,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: - \isa{{\isasymlambda}x\ y{\isachardot}\ x} is a well-typed term. + \medskip This sentence demonstrates quotations and antiquotations: + \isa{{\isasymlambda}x\ y{\isachardot}\ x} is a well-typed term. \medskip\noindent The output above was produced as follows: \begin{ttbox} @@ -639,22 +629,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~\isa{{\isasymlambda}} reveals that Isabelle printed this term, - after parsing and type-checking. Document preparation - enables symbolic output by default. + symbol~\isa{{\isasymlambda}} 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 \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. 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 \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. 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 @@ -690,8 +679,9 @@ For example, \texttt{\at}\verb,{text "\\"}, produces \isa{{\isasymforall}{\isasymexists}}, 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.% \end{isamarkuptext}% \isamarkuptrue% % @@ -707,9 +697,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} @@ -719,18 +709,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,, 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,, (see \texttt{isabelle.sty} for working examples). Control symbols are slightly more difficult to get right, though. @@ -764,23 +754,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 @@ -798,8 +787,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:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}x\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isacharless}\ x\ {\isacharasterisk}\ x{\isachardoublequote}\isanewline @@ -814,18 +803,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,),