# HG changeset patch # User wenzelm # Date 1011113668 -3600 # Node ID 7d67b065925e3501b1b3700c3d154637525d8314 # Parent fb3f9887d0b72e9a4fd7128399e899d8d3d93990 tuned; diff -r fb3f9887d0b7 -r 7d67b065925e doc-src/TutorialI/Documents/Documents.thy --- 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 "\"} 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 "\"} 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 "\"} and @{text - "\"}) 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 "\"} and @{text "\"}) 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,, symbol as~@{text \}. + 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~@{text \}. 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>\, is output as @{text "A\<^sup>\"}. - \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 \} 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 @{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 \ 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 \ 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 \ 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) \ sim"} by @{text "x \ y"}. + relational notation for membership in a set of pair, replacing \ + @{text "(x, y) \ sim"} by @{text "x \ 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) \ 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 \}~\verb,", or \verb,{,\verb,*,~@{text \}~\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 \} reveals that Isabelle printed this term, - after parsing and type-checking. Document preparation - enables symbolic output by default. + symbol~@{text \} 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 @@ "\\"}, 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,, 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. @@ -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 \ (0::int) \ 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,),