1.1 --- a/doc-src/TutorialI/basics.tex	Mon Jun 06 19:09:49 2005 +0200
     1.2 +++ b/doc-src/TutorialI/basics.tex	Mon Jun 06 21:20:54 2005 +0200
     1.3 @@ -77,24 +77,27 @@
     1.4  constructs is found in the Isabelle/Isar Reference
     1.5  Manual~\cite{isabelle-isar-ref}.
     1.6  
     1.7 -HOL's theory collection is available online at
     1.8 -\begin{center}\small
     1.9 -    \url{http://isabelle.in.tum.de/library/HOL/}
    1.10 -\end{center}
    1.11 -and is recommended browsing. Note that most of the theories 
    1.12 -are based on classical Isabelle without the Isar extension. This means that
    1.13 -they look slightly different than the theories in this tutorial, and that all
    1.14 -proofs are in separate ML files.
    1.15 -
    1.16  \begin{warn}
    1.17    HOL contains a theory \thydx{Main}, the union of all the basic
    1.18    predefined theories like arithmetic, lists, sets, etc.  
    1.19    Unless you know what you are doing, always include \isa{Main}
    1.20    as a direct or indirect parent of all your theories.
    1.21  \end{warn}
    1.22 +HOL's theory collection is available online at
    1.23 +\begin{center}\small
    1.24 +    \url{http://isabelle.in.tum.de/library/HOL/}
    1.25 +\end{center}
    1.26 +and is recommended browsing.
    1.27  There is also a growing Library~\cite{HOL-Library}\index{Library}
    1.28  of useful theories that are not part of \isa{Main} but can be included
    1.29 -among the parents of a theory and will then be loaded automatically.%
    1.30 +among the parents of a theory and will then be loaded automatically.
    1.31 +
    1.32 +For the more adventurous, there is the \emph{Archive of Formal Proofs},
    1.33 +a journal-like collection of more advanced Isabelle theories:
    1.34 +\begin{center}\small
    1.35 +    \url{http://afp.sourceforge.net/}
    1.36 +\end{center}
    1.37 +We hope that you will contribute to it yourself one day.%
    1.38  \index{theories|)}
    1.39  
    1.40  
    1.41 @@ -137,18 +140,9 @@
    1.42    the user, Isabelle infers the type of all variables automatically (this is
    1.43    called \bfindex{type inference}) and keeps quiet about it. Occasionally
    1.44    this may lead to misunderstandings between you and the system. If anything
    1.45 -  strange happens, we recommend that you set the flag\index{flags}
    1.46 -  \isa{show_types}\index{*show_types (flag)}.  
    1.47 -  Isabelle will then display type information
    1.48 -  that is usually suppressed.  Simply type
    1.49 -\begin{ttbox}
    1.50 -ML "set show_types"
    1.51 -\end{ttbox}
    1.52 -
    1.53 -\noindent
    1.54 -This can be reversed by \texttt{ML "reset show_types"}. Various other flags,
    1.55 -which we introduce as we go along, can be set and reset in the same manner.%
    1.56 -\index{flags!setting and resetting}
    1.57 +  strange happens, we recommend that you ask Isabelle to display all type
    1.58 +  information. This is best done through the Proof General interface; see
    1.59 +  \S\ref{sec:interface} for details.
    1.60  \end{warn}%
    1.61  \index{types|)}
    1.62  
    1.63 @@ -308,6 +302,7 @@
    1.64  \index{variables|)}
    1.65  
    1.66  \section{Interaction and Interfaces}
    1.67 +\label{sec:interface}
    1.68  
    1.69  Interaction with Isabelle can either occur at the shell level or through more
    1.70  advanced interfaces. To keep the tutorial independent of the interface, we
    1.71 @@ -320,16 +315,26 @@
    1.72  Isabelle/Isar is the Emacs-based \bfindex{Proof
    1.73    General}~\cite{proofgeneral,Aspinall:TACAS:2000}.
    1.74  
    1.75 -Some interfaces (including the shell level) offer special fonts with
    1.76 -mathematical symbols. For those that do not, remember that \textsc{ascii}-equivalents
    1.77 -are shown in table~\ref{tab:ascii} in the appendix.
    1.78 +\begin{pgnote}
    1.79 +Proof General specific information is always displayed in paragraphs
    1.80 +identified by this miniature Proof General icon.
    1.81  
    1.82 -Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} 
    1.83 -Commands may but need not be terminated by semicolons.
    1.84 -At the shell level it is advisable to use semicolons to enforce that a command
    1.85 -is executed immediately; otherwise Isabelle may wait for the next keyword
    1.86 -before it knows that the command is complete.
    1.87 +On particularly nice feature of Proof General is its support for a special
    1.88 +fonts with mathematical symbols. Most symbols have
    1.89 +\textsc{ascii}-equivalents: for example, you can enter either \verb!&!
    1.90 +or \verb!\<and>! to obtain $\land$. For a list of the most frequent symbols
    1.91 +see table~\ref{tab:ascii} in the appendix.
    1.92 +\end{pgnote}
    1.93  
    1.94 +\begin{pgnote}
    1.95 +Proof General offers an \texttt{Isabelle} menu for displaying information
    1.96 +and setting flags. A particularly useful flag is \texttt{Show Types}
    1.97 +which causes Isabelle to output the type information that is usually
    1.98 +suppressed. This is indispensible in case of errors of all kinds
    1.99 +because often the types reveal the source of the problem. Once you have
   1.100 +diagnosed the problem you may no longer want to see the types because they
   1.101 +clutter all output. Simply reset the flag.
   1.102 +\end{pgnote}
   1.103  
   1.104  \section{Getting Started}
   1.105  

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