--- a/doc-src/TutorialI/Documents/document/Documents.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Documents}%
-\isamarkupfalse%
%
\isadelimtheory
%
@@ -134,26 +133,24 @@
printable symbol, respectively. For example, \verb,A\<^sup>\<star>, is
output as \isa{A\isactrlsup {\isasymstar}}.
- A number of symbols are considered letters by the Isabelle lexer
- and can be used as part of identifiers. These are the greek letters
- \isa{{\isasymalpha}} (\verb+\+\verb+<alpha>+), \isa{{\isasymbeta}}, etc apart from
- \isa{{\isasymlambda}}, caligraphic letters like \isa{{\isasymA}}
- (\verb+\+\verb+<A>+) and \isa{{\isasymAA}} (\verb+\+\verb+<AA>+),
- and the special control symbols \verb+\+\verb+<^isub>+ and
- \verb+\+\verb+<^isup>+ for single letter sub and super scripts. This
- means that the input
+ A number of symbols are considered letters by the Isabelle lexer and
+ can be used as part of identifiers. These are the greek letters
+ \isa{{\isasymalpha}} (\verb+\+\verb+<alpha>+), \isa{{\isasymbeta}}
+ (\verb+\+\verb+<beta>+), etc. (excluding \isa{{\isasymlambda}}),
+ special letters like \isa{{\isasymA}} (\verb+\+\verb+<A>+) and \isa{{\isasymAA}} (\verb+\+\verb+<AA>+), and the control symbols
+ \verb+\+\verb+<^isub>+ and \verb+\+\verb+<^isup>+ for single letter
+ sub and super scripts. This means that the input
\medskip
- {\small\noindent \verb,\,\verb,<forall>\,\verb,<alpha>\<^isub>1.\,\verb,<alpha>\<^isub>1=\,\verb,<Pi>\<^isup>\<A>,}
+ {\small\noindent \verb,\,\verb,<forall>\,\verb,<alpha>\<^isub>1.,~\verb,\,\verb,<alpha>\<^isub>1 = \,\verb,<Pi>\<^isup>\<A>,}
\medskip
\noindent is recognized as the term \isa{{\isasymforall}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isachardot}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isacharequal}\ {\isasymPi}\isactrlisup {\isasymA}}
- by Isabelle. Note that \isa{{\isasymPi}\isactrlisup {\isasymA}} is a single entity like
- \isa{PA}, not an exponentiation.
+ by Isabelle. Note that \isa{{\isasymPi}\isactrlisup {\isasymA}} is a single
+ syntactic entity, not an exponentiation.
-
- \medskip Replacing our definition of \isa{xor} by the following
- specifies an Isabelle symbol for the new operator:%
+ \medskip Replacing our previous definition of \isa{xor} by the
+ following specifies an Isabelle symbol for the new operator:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -425,10 +422,7 @@
location of the ultimate results. The above dry run should be able
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 in doubt one may
- fall back on DVI output by changing \texttt{usedir} options in
- \texttt{IsaMakefile} \cite{isabelle-sys}.}
+ technical problems of the {\LaTeX} installation.
\medskip The detailed arrangement of the session sources is as
follows.
@@ -826,37 +820,54 @@
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. 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, of course.
-
- In this example, we hide a theory's \isakeyword{theory} and
- \isakeyword{end} brackets:
-
- \medskip
+ \medskip Theory output may be suppressed more selectively, either
+ via \bfindex{tagged command regions} or \bfindex{ignored material}.
- \begin{tabular}{l}
- \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
- \texttt{theory T} \\
- \texttt{imports Main} \\
- \texttt{begin} \\
- \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
- ~~$\vdots$ \\
- \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
- \texttt{end} \\
- \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
- \end{tabular}
+ Tagged command regions works by annotating commands with named tags,
+ which correspond to certain {\LaTeX} markup that tells how to treat
+ particular parts of a document when doing the actual type-setting.
+ By default, certain Isabelle/Isar commands are implicitly marked up
+ using the predefined tags ``\emph{theory}'' (for theory begin and
+ end), ``\emph{proof}'' (for proof commands), and ``\emph{ML}'' (for
+ commands involving ML code). Users may add their own tags using the
+ \verb,%,\emph{tag} notation right after a command name. In the
+ subsequent example we hide a particularly irrelevant proof:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isacharequal}\ x{\isachardoublequoteclose}%
+\isadeliminvisible
+\ %
+\endisadeliminvisible
+%
+\isataginvisible
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp{\isacharparenright}%
+\endisataginvisible
+{\isafoldinvisible}%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\begin{isamarkuptext}%
+The original source has been ``\verb,lemma "x = x" by %invisible (simp),''.
+ Tags observe the structure of proofs; adjacent commands with the
+ same tag are joined into a single region. The Isabelle document
+ preparation system allows the user to specify how to interpret a
+ tagged region, in order to keep, drop, or fold the corresponding
+ parts of the document. See the \emph{Isabelle System Manual}
+ \cite{isabelle-sys} for further details, especially on
+ \texttt{isatool usedir} and \texttt{isatool document}.
- \medskip
-
- 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:%
+ Ignored material is specified by delimiting the original formal
+ source with special source comments
+ \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
+ \verb,(,\verb,*,\verb,>,\verb,*,\verb,),. These parts are stripped
+ before the type-setting phase, without affecting the formal checking
+ of the theory, of course. For example, we may hide parts of a proof
+ that seem unfit for general public inspection. The following
+ ``fully automatic'' proof is actually a fake:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
@@ -877,7 +888,7 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-\noindent Here the real source of the proof has been as follows:
+\noindent The real source of the proof has been as follows:
\begin{verbatim}
by (auto(*<*)simp add: zero_less_mult_iff(*>*))
@@ -887,23 +898,7 @@
\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.
-
-% I removed this because the page overflowed and I disagree a little. TN
-%
-% 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.
-
- \medskip Some technical subtleties of the
- \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
- elements need to be kept in mind, too --- the system performs few
- sanity checks here. Arguments of markup commands and formal
- comments must not be hidden, otherwise presentation fails. Open and
- close parentheses need to be inserted carefully; it is easy to hide
- the wrong parts, especially after rearranging the theory text.%
+ questionable axioms.%
\end{isamarkuptext}%
\isamarkuptrue%
%