--- a/doc-src/TutorialI/Documents/document/Documents.tex Mon Jan 14 16:09:25 2002 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Mon Jan 14 16:09:29 2002 +0100
@@ -297,7 +297,52 @@
proofs formally, the theory sources are turned into typesetting
instructions in a schematic manner. This enables users to write
authentic reports on theory developments with little effort, where
- most consistency checks are handled by the system.%
+ most consistency checks are handled by the system.
+
+ Here is an example to illustrate the idea of Isabelle document
+ preparation.
+
+ \bigskip The following datatype definition of \isa{{\isacharprime}a\ bintree}
+ models binary trees with nodes being decorated by elements of type
+ \isa{{\isacharprime}a}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{datatype}\ {\isacharprime}a\ bintree\ {\isacharequal}\isanewline
+\ \ Leaf\ {\isacharbar}\ Branch\ {\isacharprime}a\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+\noindent The datatype induction rule generated here is of the form
+ \begin{isabelle}%
+{\isasymlbrakk}P\ Leaf{\isacharsemicolon}\isanewline
+\isaindent{\ \ \ }{\isasymAnd}a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isachardot}\isanewline
+\isaindent{\ \ \ \ \ \ }{\isasymlbrakk}P\ bintree{\isadigit{1}}{\isacharsemicolon}\ P\ bintree{\isadigit{2}}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Branch\ a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isacharparenright}{\isasymrbrakk}\isanewline
+{\isasymLongrightarrow}\ P\ bintree%
+\end{isabelle}
+
+ \bigskip The above document output has been produced by the
+ following theory specification:
+
+ \begin{ttbox}
+ text {\ttlbrace}*
+ The following datatype definition of {\at}{\ttlbrace}text "'a bintree"{\ttrbrace}
+ models binary trees with nodes being decorated by elements
+ of type {\at}{\ttlbrace}typ 'a{\ttrbrace}.
+ *{\ttrbrace}
+
+ datatype 'a bintree =
+ Leaf | Branch 'a "'a bintree" "'a bintree"
+
+ 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}
+
+ Here we have augmented the theory by formal comments (via
+ \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}%
\isamarkuptrue%
%
@@ -337,7 +382,8 @@
\texttt{IsaMakefile} \cite{isabelle-sys}.}
\medskip The detailed arrangement of the session sources is as
- follows; advanced
+ follows. This may be ignored in the beginning, but some of these
+ files need to be edited in realistic applications.
\begin{itemize}
@@ -473,10 +519,10 @@
\renewcommand{\isamarkupheader}[1]{\chapter{#1}}
\end{verbatim}
- \noindent That particular modification requires to change the
- default \verb,\documentclass{article}, in \texttt{root.tex} to
- something that supports the notion of chapters in the first place,
- such as \verb,\documentclass{report},.
+ \noindent That particular modification requires change to the
+ document class given in \texttt{root.tex} to something that supports
+ the notion of chapters in the first place, such as
+ \verb,\documentclass{report},.
\medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
hold the name of the current theory context. This is particularly
@@ -493,12 +539,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Formal Comments and Antiquotations%
+\isamarkupsubsection{Formal Comments and Antiquotations \label{sec:doc-prep-text}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Isabelle source comments, which are of the form
+Isabelle \bfindex{source comments}, which are of the form
\verb,(,\verb,*,~\dots~\verb,*,\verb,),, essentially act like white
space and do not really contribute to the content. They mainly
serve technical purposes to mark certain oddities in the raw input