updating...

--- a/doc-src/TutorialI/basics.tex	Mon Jun 06 19:09:49 2005 +0200
+++ b/doc-src/TutorialI/basics.tex	Mon Jun 06 21:20:54 2005 +0200
@@ -77,24 +77,27 @@
 constructs is found in the Isabelle/Isar Reference
 Manual~\cite{isabelle-isar-ref}.
 
-HOL's theory collection is available online at
-\begin{center}\small
-    \url{http://isabelle.in.tum.de/library/HOL/}
-\end{center}
-and is recommended browsing. Note that most of the theories 
-are based on classical Isabelle without the Isar extension. This means that
-they look slightly different than the theories in this tutorial, and that all
-proofs are in separate ML files.
-
 \begin{warn}
   HOL contains a theory \thydx{Main}, the union of all the basic
   predefined theories like arithmetic, lists, sets, etc.  
   Unless you know what you are doing, always include \isa{Main}
   as a direct or indirect parent of all your theories.
 \end{warn}
+HOL's theory collection is available online at
+\begin{center}\small
+    \url{http://isabelle.in.tum.de/library/HOL/}
+\end{center}
+and is recommended browsing.
 There is also a growing Library~\cite{HOL-Library}\index{Library}
 of useful theories that are not part of \isa{Main} but can be included
-among the parents of a theory and will then be loaded automatically.%
+among the parents of a theory and will then be loaded automatically.
+
+For the more adventurous, there is the \emph{Archive of Formal Proofs},
+a journal-like collection of more advanced Isabelle theories:
+\begin{center}\small
+    \url{http://afp.sourceforge.net/}
+\end{center}
+We hope that you will contribute to it yourself one day.%
 \index{theories|)}
 
 
@@ -137,18 +140,9 @@
   the user, Isabelle infers the type of all variables automatically (this is
   called \bfindex{type inference}) and keeps quiet about it. Occasionally
   this may lead to misunderstandings between you and the system. If anything
-  strange happens, we recommend that you set the flag\index{flags}
-  \isa{show_types}\index{*show_types (flag)}.  
-  Isabelle will then display type information
-  that is usually suppressed.  Simply type
-\begin{ttbox}
-ML "set show_types"
-\end{ttbox}
-
-\noindent
-This can be reversed by \texttt{ML "reset show_types"}. Various other flags,
-which we introduce as we go along, can be set and reset in the same manner.%
-\index{flags!setting and resetting}
+  strange happens, we recommend that you ask Isabelle to display all type
+  information. This is best done through the Proof General interface; see
+  \S\ref{sec:interface} for details.
 \end{warn}%
 \index{types|)}
 
@@ -308,6 +302,7 @@
 \index{variables|)}
 
 \section{Interaction and Interfaces}
+\label{sec:interface}
 
 Interaction with Isabelle can either occur at the shell level or through more
 advanced interfaces. To keep the tutorial independent of the interface, we
@@ -320,16 +315,26 @@
 Isabelle/Isar is the Emacs-based \bfindex{Proof
   General}~\cite{proofgeneral,Aspinall:TACAS:2000}.
 
-Some interfaces (including the shell level) offer special fonts with
-mathematical symbols. For those that do not, remember that \textsc{ascii}-equivalents
-are shown in table~\ref{tab:ascii} in the appendix.
+\begin{pgnote}
+Proof General specific information is always displayed in paragraphs
+identified by this miniature Proof General icon.
 
-Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} 
-Commands may but need not be terminated by semicolons.
-At the shell level it is advisable to use semicolons to enforce that a command
-is executed immediately; otherwise Isabelle may wait for the next keyword
-before it knows that the command is complete.
+On particularly nice feature of Proof General is its support for a special
+fonts with mathematical symbols. Most symbols have
+\textsc{ascii}-equivalents: for example, you can enter either \verb!&!
+or \verb!\<and>! to obtain $\land$. For a list of the most frequent symbols
+see table~\ref{tab:ascii} in the appendix.
+\end{pgnote}
 
+\begin{pgnote}
+Proof General offers an \texttt{Isabelle} menu for displaying information
+and setting flags. A particularly useful flag is \texttt{Show Types}
+which causes Isabelle to output the type information that is usually
+suppressed. This is indispensible in case of errors of all kinds
+because often the types reveal the source of the problem. Once you have
+diagnosed the problem you may no longer want to see the types because they
+clutter all output. Simply reset the flag.
+\end{pgnote}
 
 \section{Getting Started}
 

--- a/doc-src/TutorialI/preface.tex	Mon Jun 06 19:09:49 2005 +0200
+++ b/doc-src/TutorialI/preface.tex	Mon Jun 06 21:20:54 2005 +0200
@@ -2,20 +2,10 @@
 \markboth{Preface}{Preface}
 
 This volume is a self-contained introduction to interactive proof
-in higher-order logic (HOL), using the proof assistant Isabelle 2002. 
-Compared with existing Isabelle documentation,
-it provides a direct route into higher-order logic, which most people
-prefer these days. It bypasses first-order logic and minimizes
-discussion of meta-theory.  It is written for potential users rather
+in higher-order logic (HOL), using the proof assistant Isabelle. 
+It is written for potential users rather
 than for our colleagues in the research world.
 
-Another departure from previous documentation is that we describe Markus
-Wenzel's proof script notation instead of ML tactic scripts.  The latter
-make it easier to introduce new tactics on the fly, but hardly anybody
-does that.  Wenzel's dedicated syntax is elegant, replacing for example
-eight simplification tactics with a single method, namely \isa{simp},
-with associated options.
-
 The book has three parts.  
 \begin{itemize}
 \item 
@@ -33,16 +23,14 @@
 examples concerns the theory of model checking, and another is drawn
 from a classic textbook on formal languages.
 \item 
-The third part, \textbf{Advanced Material}, describes a variety of
-other topics.  Among these are the real numbers, records and
-overloading.  Esoteric techniques are described involving induction and
-recursion.  A whole chapter is devoted to an extended example: the
-verification of a security protocol.
+The third part, \textbf{Advanced Material}, describes a variety of other
+topics.  Among these are the real numbers, records and overloading.  Advanced
+techniques for induction and recursion are described.  A whole chapter is
+devoted to an extended example: the verification of a security protocol.
 \end{itemize}
 
 The typesetting relies on Wenzel's theory presentation tools.  An
 annotated source file is run, typesetting the theory
-% and any requested Isabelle responses
 in the form of a \LaTeX\ source file.  This book is derived almost entirely
 from output generated in this way.  The final chapter of Part~I explains how
 users may produce their own formal documents in a similar fashion.
@@ -57,8 +45,7 @@
 In order to run Isabelle, you will need a Standard ML compiler.  We recommend
 \hfootref{http://www.polyml.org/}{Poly/ML}, which is free and gives the best
 performance.  The other fully supported compiler is
-\hfootref{http://cm.bell-labs.com/cm/cs/what/smlnj/index.html}{Standard ML of
-  New Jersey}.
+\hfootref{http://www.smlnj.org/index.html}{Standard ML of New Jersey}.
 
 This tutorial owes a lot to the constant discussions with and the valuable
 feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf
@@ -69,7 +56,7 @@
 and Tanja Vos.
 
 The research has been funded by many sources, including the {\sc dfg} grants
-Ni~491/2, Ni~491/3, Ni~491/4 and the {\sc epsrc} grants GR\slash K57381,
-GR\slash K77051, GR\slash M75440, GR\slash R01156\slash 01 and by the
-\textsc{esprit} working groups 21900 and IST-1999-29001 (the \emph{Types}
-project).
+NI~491/2, NI~491/3, NI~491/4, NI~491/6, {\sc bmbf} project Verisoft, the {\sc
+epsrc} grants GR/K57381, GR/K77051, GR/M75440, GR/R01156/01 GR/S57198/01 and
+by the \textsc{esprit} working groups 21900 and IST-1999-29001 (the
+\emph{Types} project).