# HG changeset patch
# User wenzelm
# Date 1010321275 -3600
# Node ID 001d10bbc61b3cd3f1e5381326454945e1b004b4
# Parent  fa2e8a8faaec3fccf204ea7c8f4be12569808280
updated;

diff -r fa2e8a8faaec -r 001d10bbc61b doc-src/TutorialI/Documents/document/Documents.tex
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Sun Jan 06 13:47:26 2002 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Sun Jan 06 13:47:55 2002 +0100
@@ -3,7 +3,7 @@
 \def\isabellecontext{Documents}%
 \isamarkupfalse%
 %
-\isamarkupsection{Concrete syntax \label{sec:concrete-syntax}%
+\isamarkupsection{Concrete Syntax \label{sec:concrete-syntax}%
 }
 \isamarkuptrue%
 %
@@ -27,7 +27,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Infix annotations%
+\isamarkupsubsection{Infix Annotations%
 }
 \isamarkuptrue%
 %
@@ -85,7 +85,7 @@
   \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
   always demand explicit parentheses.
-  
+
   Many binary operations observe the associative law, so the exact
   grouping does not matter.  Nevertheless, formal statements need be
   given in a particular format, associativity needs to be treated
@@ -108,7 +108,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Mathematical symbols \label{sec:thy-present-symbols}%
+\isamarkupsubsection{Mathematical Symbols \label{sec:thy-present-symbols}%
 }
 \isamarkuptrue%
 %
@@ -218,7 +218,7 @@
 \isacommand{syntax}\ {\isacharparenleft}xsymbols\ \isakeyword{output}{\isacharparenright}\isanewline
 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
 %
-\isamarkupsubsection{Prefix annotations%
+\isamarkupsubsection{Prefix Annotations%
 }
 \isamarkuptrue%
 %
@@ -261,7 +261,7 @@
 \isacommand{consts}\isanewline
 \ \ currency\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}currency\ {\isasymRightarrow}\ nat{\isachardoublequote}\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymcurrency}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
 %
-\isamarkupsubsection{Syntax translations \label{sec:def-translations}%
+\isamarkupsubsection{Syntax Translations \label{sec:def-translations}%
 }
 \isamarkuptrue%
 %
@@ -291,7 +291,7 @@
 parsing or printing.  This tutorial will not cover the details of
 translations.  We have mentioned the concept merely because it
 crops up occasionally; a number of HOL's built-in constructs are defined
-via translations.  Translations are preferable to definitions when the new 
+via translations.  Translations are preferable to definitions when the new
 concept is a trivial variation on an existing one.  For example, we
 don't need to derive new theorems about \isa{{\isasymnoteq}}, since existing theorems
 about \isa{{\isacharequal}} still apply.%
@@ -300,7 +300,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{Document preparation%
+\isamarkupsection{Document Preparation%
 }
 \isamarkuptrue%
 %
@@ -332,7 +332,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Isabelle sessions%
+\isamarkupsubsection{Isabelle Sessions%
 }
 \isamarkuptrue%
 %
@@ -381,7 +381,7 @@
   with the generated document appearing in its proper place (within
   \verb,~/isabelle/browser_info,).
 
-  In practive, users may want to have \texttt{isatool mkdir} generate
+  In practice, users may want to have \texttt{isatool mkdir} generate
   an initial working setup without further ado.  For example, an empty
   session \texttt{MySession} derived from \texttt{HOL} may be produced
   as follows:
@@ -403,7 +403,10 @@
   \texttt{MySession}, and the file \texttt{MySession/ROOT.ML}
   accordingly.  \texttt{MySession/document/root.tex} should be also
   adapted at some point; the generated version is mostly
-  self-explanatory.
+  self-explanatory.  The default versions includes the
+  \texttt{isabelle} (mandatory) and \texttt{isabellesym} (required for
+  mathematical symbols); further packages may required, e.g.\ for
+  unusual Isabelle symbols.
 
   Realistic applications may demand additional files in
   \texttt{MySession/document} for the {\LaTeX} stage, such as
@@ -420,7 +423,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Structure markup%
+\isamarkupsubsection{Structure Markup%
 }
 \isamarkuptrue%
 %
@@ -429,7 +432,9 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-The large-scale structure of Isabelle documents closely follows
+FIXME \verb,\label, within sections;
+
+  The large-scale structure of Isabelle documents closely follows
   {\LaTeX} convention, with chapters, sections, subsubsections etc.
   The formal Isar language includes separate structure \bfindex{markup
   commands}, which do not effect the formal content of a theory (or
@@ -464,7 +469,8 @@
   above.
 
   \medskip The following source fragment illustrates structure markup
-  of a theory.
+  of a theory.  Note that {\LaTeX} labels may well be included inside
+  of section headings as well.
 
   \begin{ttbox}
   header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
@@ -476,25 +482,26 @@
   consts
     foo :: \dots
     bar :: \dots
+
   defs \dots
-    
+
   subsection {\ttlbrace}* Derived rules *{\ttrbrace}
 
   lemma fooI: \dots
   lemma fooE: \dots
 
-  subsection {\ttlbrace}* Main theorem *{\ttrbrace}
+  subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace}
 
   theorem main: \dots
 
   end
   \end{ttbox}
 
-  \medskip In realistic applications, users may well want to change
-  the meaning of some markup commands, typically via appropriate use
-  of \verb,\renewcommand, in \texttt{root.tex}.  The
-  \verb,\isamarkupheader, is a good candidate for some adaption, e.g.\
-  moving it up in the hierarchy to become \verb,\chapter,.
+  Users may occasionally want to change the meaning of some markup
+  commands, typically via appropriate use of \verb,\renewcommand, in
+  \texttt{root.tex}.  The \verb,\isamarkupheader, is a good candidate
+  for some adaption, e.g.\ moving it up in the hierarchy to become
+  \verb,\chapter,.
 
 \begin{verbatim}
   \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
@@ -503,12 +510,11 @@
   Certainly, this requires to change the default
   \verb,\documentclass{article}, in \texttt{root.tex} to something
   that supports the notion of chapters in the first place, e.g.\
-  \texttt{report} or \texttt{book}.
+  \verb,\documentclass{report},.
 
-  \medskip For each generated theory output the {\LaTeX} macro
-  \verb,\isabellecontext, holds the name of the formal context.  This
-  is particularly useful for document headings or footings, e.g.\ like
-  this:
+  \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
+  hold the name of the current theory context.  This is particularly
+  useful for document headings or footings, e.g.\ like this:
 
 \begin{verbatim}
   \renewcommand{\isamarkupheader}[1]%
@@ -516,21 +522,21 @@
 \end{verbatim}
 
   \noindent Make sure to include something like
-  \verb,\pagestyle{headings}, in \texttt{root.tex} as well.  Moreover,
-  the document should have more than 2 pages.%
+  \verb,\pagestyle{headings}, in \texttt{root.tex}; the document
+  should have more than 2 pages to show the effect.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Formal comments and antiquotations%
+\isamarkupsubsection{Formal Comments and Antiquotations%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Comments of the form \verb,(*,~\dots~\verb,*),%
+Comments of the form \verb,(,\verb,*,~\dots~\verb,*,\verb,),%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Symbols and characters%
+\isamarkupsubsection{Symbols and Characters%
 }
 \isamarkuptrue%
 %
@@ -539,15 +545,63 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Suppressing output%
+\isamarkupsubsection{Suppressing Output%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME \verb,no_document,
+By default Isabelle's document system generates a {\LaTeX} source
+  file for each theory that happens to get loaded during the session.
+  The generated \texttt{session.tex} file will include all of these in
+  order of appearance, which in turn gets included by the standard
+  \texttt{root.tex} file.  Certainly one may change the order of
+  appearance or suppress unwanted theories by ignoring
+  \texttt{session.tex} and include individual files in
+  \texttt{root.tex} by hand.  On the other hand, such an arrangement
+  requires additional efforts for maintenance.
+
+  Alternatively, one may tune the theory loading process in
+  \texttt{ROOT.ML}: traversal of the theory dependency graph may be
+  fine-tuned by adding further \verb,use_thy, invocations, although
+  topological sorting needs to be preserved.  Moreover, the ML
+  operator \verb,no_document, temporarily disables document generation
+  while executing a theory loader command; the usage is like this:
+
+\begin{verbatim}
+  no_document use_thy "Aux";
+\end{verbatim}
 
-  FIXME \verb,(,\verb,*,\verb,<,\verb,*,\verb,),
-  \verb,(,\verb,*,\verb,>,\verb,*,\verb,),%
+  Theory output may be also suppressed \emph{partially} as well.
+  Typical applications include research papers or slides based on
+  formal developments --- these usually do not show the full formal
+  content.  The special source comments
+  \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
+  \verb,(,\verb,*,\verb,>,\verb,*,\verb,), are interpreted by the
+  document generator as open and close parenthesis for
+  \bfindex{ignored material}.  Any text inside of (potentially nested)
+  \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\dots~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
+  parentheses is just ignored from the output --- after correct formal
+  checking.
+
+  In the following example we suppress the slightly formalistic
+  \isakeyword{theory} and \isakeyword{end} part of a theory text.
+
+  \medskip
+
+  \begin{tabular}{l}
+  \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
+  \texttt{theory A = Main:} \\
+  \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
+  ~~$\vdots$ \\
+  \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
+  \texttt{end} \\
+  \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
+  \end{tabular}
+
+  \medskip
+
+  Ignoring portions of printed text like this demands some special
+  care. FIXME%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isamarkupfalse%
diff -r fa2e8a8faaec -r 001d10bbc61b doc-src/TutorialI/tutorial.ind
--- a/doc-src/TutorialI/tutorial.ind	Sun Jan 06 13:47:26 2002 +0100
+++ b/doc-src/TutorialI/tutorial.ind	Sun Jan 06 13:47:55 2002 +0100
@@ -265,6 +265,7 @@
   \item \isa {iff} (attribute), 88, 100, 128
   \item \isa {iffD1} (theorem), \bold{92}
   \item \isa {iffD2} (theorem), \bold{92}
+  \item ignored material, \bold{61}
   \item image
     \subitem under a function, \bold{109}
     \subitem under a relation, \bold{110}