# HG changeset patch
# User wenzelm
# Date 955402579 -7200
# Node ID dfe444b748aa1bed357244dab61db0d4021b2068
# Parent  9d3e8c4a02878787ac2a8c944e0a496425c1b247
improved document preparation;

diff -r 9d3e8c4a0287 -r dfe444b748aa doc-src/IsarRef/intro.tex
--- a/doc-src/IsarRef/intro.tex	Sat Apr 08 19:38:19 2000 +0200
+++ b/doc-src/IsarRef/intro.tex	Mon Apr 10 23:36:19 2000 +0200
@@ -136,7 +136,61 @@
 emerging Isabelle/Isar document.
 
 
-\section{How to write Isar proofs anyway?}
+\subsection{Document preparation}
+
+Isabelle/Isar provides a simple document preparation system based on current
+(PDF) {\LaTeX} technology, with full support of hyper-links (both local
+references and URLs), bookmarks, thumbnails etc.  Thus the results are equally
+well suited for WWW browsing and as printed copies.
+
+\medskip
+
+Isabelle generates {\LaTeX} output as part of the run of a \emph{logic
+  session} (see also \cite{isabelle-sys}).  Getting started with a working
+configuration for common situations is quite easy by using the Isabelle
+\texttt{mkdir} and \texttt{make} tools.  Just invoke
+\begin{ttbox}
+  isatool mkdir -d Foo
+\end{ttbox}
+to setup a separate directory for session \texttt{Foo}.\footnote{It is safe to
+  experiment, since \texttt{isatool mkdir} never overwrites existing files.}
+Ensure that \texttt{Foo/ROOT.ML} loads all theories required for this session.
+Furthermore \texttt{Foo/document/root.tex} should include any special {\LaTeX}
+macro packages required for your document (the default is usually sufficient
+as a start).
+
+The session is controlled by a separate \texttt{IsaMakefile} (with very crude
+source dependencies only by default).  This file is located one level up from
+the \texttt{Foo} directory location.  At that point just invoke
+\begin{ttbox}
+  isatool make Foo
+\end{ttbox}
+to run the \texttt{Foo} session, with browser information and document
+preparation enabled.  Unless any errors are reported by Isabelle or {\LaTeX},
+the output will appear inside the directory indicated by \texttt{isatool
+  getenv ISABELLE_BROWSER_INFO}, with the logical session prefix added (e.g.\ 
+\texttt{HOL/Foo}).  Note that the \texttt{index.html} located there provides a
+link to the finished {\LaTeX} document, too.
+
+Note that this really is batch processing --- better let Isabelle check your
+theory and proof developments beforehand in interactive mode.
+
+\medskip
+
+You may also consider to tune the \texttt{usedir} options in
+\texttt{IsaMakefile}, for example to change the output format from
+\texttt{dvi} to \texttt{pdf}, or activate the \texttt{-D document} option in
+order to preserve a copy of the generated {\LaTeX} sources.  The latter
+feature is very useful for debugging {\LaTeX} errors, while avoiding repeated
+runs of Isabelle.
+
+\medskip
+
+See \emph{The Isabelle System Manual} \cite{isabelle-sys} for further details
+on Isabelle logic sessions and theory presentation.
+
+
+\subsection{How to write Isar proofs anyway?}
 
 This is one of the key questions, of course.  Isar offers a rather different
 approach to formal proof documents than plain old tactic scripts.  Experienced
diff -r 9d3e8c4a0287 -r dfe444b748aa doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Sat Apr 08 19:38:19 2000 +0200
+++ b/doc-src/IsarRef/pure.tex	Mon Apr 10 23:36:19 2000 +0200
@@ -131,18 +131,20 @@
     package to be included in {\LaTeX}, of course.}
 \end{descr}
 
-Any markup command (except $\isarkeyword{text_raw}$) corresponds to a {\LaTeX}
-macro with the name prefixed by \verb,\isamarkup, (e.g.\ 
-\verb,\isamarkupchapter, for $\isarkeyword{chapter}$). The \railqtoken{text}
-argument is passed to that macro unchanged, i.e.\ further {\LaTeX} commands
-may be included here as well.
+Any of these markup elements corresponds to a {\LaTeX} command with the name
+prefixed by \verb,\isamarkup,.  For the sectioning commands this is a plain
+macro with a single argument, e.g.\ \verb,\isamarkupchapter{,\dots\verb,}, for
+$\isarkeyword{chapter}$.  The $\isarkeyword{text}$ markup results in a
+{\LaTeX} environment \verb,\begin{isamarkuptext}, {\dots}
+  \verb,\end{isamarkuptext},, while $\isarkeyword{text_raw}$ causes the text
+to be inserted directly into the {\LaTeX} source.
 
 \medskip
 
 Additional markup commands are available for proofs (see
 \S\ref{sec:markup-prf}).  Also note that the $\isarkeyword{header}$
-declaration (see \S\ref{sec:begin-thy}) admits to insert document markup
-elements just preceding the actual theory definition.
+declaration (see \S\ref{sec:begin-thy}) admits to insert section markup just
+preceding the actual theory definition.
 
 
 \subsection{Type classes and sorts}\label{sec:classes}
@@ -475,8 +477,7 @@
 \end{matharray}
 
 These markup commands for proof mode closely correspond to the ones of theory
-mode (see \S\ref{sec:markup-thy}).  Note that $\isarkeyword{txt_raw}$ is
-special in the same way as $\isarkeyword{text_raw}$.
+mode (see \S\ref{sec:markup-thy}).
 
 \railalias{txtraw}{txt\_raw}
 \railterm{txtraw}