--- a/doc-src/Intro/intro.tex Wed Aug 13 17:24:59 2003 +0200
+++ b/doc-src/Intro/intro.tex Wed Aug 13 17:44:01 2003 +0200
@@ -31,6 +31,16 @@
\pagestyle{empty}
\begin{titlepage}
\maketitle
+\emph{Note}: this document is part of the earlier Isabelle documentation,
+which is largely superseded by the Isabelle/HOL
+\emph{Tutorial}~\cite{isa-tutorial}. It describes the old-style theory
+syntax and shows how to conduct proofs using the
+ML top level. This style of interaction is largely obsolete:
+most Isabelle proofs are now written using the Isar
+language and the Proof General interface. However, this paper contains valuable
+information that is not available elsewhere. Its examples are based
+on first-order logic rather than higher-order logic.
+
\thispagestyle{empty}
\vfill
{\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
@@ -58,12 +68,13 @@
several generic tools, such as simplifiers and classical theorem provers,
which can be applied to object-logics.
+Isabelle is a large system, but beginners can get by with a small
+repertoire of commands and a basic knowledge of how Isabelle works.
+The Isabelle/HOL \emph{Tutorial}~\cite{isa-tutorial} describes how to get started. Advanced Isabelle users will benefit from some
+knowledge of Standard~\ML{}, because Isabelle is written in \ML{};
\index{ML}
-Isabelle is a large system, but beginners can get by with a small
-repertoire of commands and a basic knowledge of how Isabelle works. Some
-knowledge of Standard~\ML{} is essential, because \ML{} is Isabelle's user
-interface. Advanced Isabelle theorem proving can involve writing \ML{}
-code, possibly with Isabelle's sources at hand. My book
+if you are prepared to writing \ML{}
+code, you can get Isabelle to do almost anything. My book
on~\ML{}~\cite{paulson-ml2} covers much material connected with Isabelle,
including a simple theorem prover. Users must be familiar with logic as
used in computer science; there are many good
@@ -83,8 +94,10 @@
treatment of quantifiers. The 1988 version added limited polymorphism and
support for natural deduction. The 1989 version included a parser and
pretty printer generator. The 1992 version introduced type classes, to
-support many-sorted and higher-order logics. The current version provides
-greater support for theories and is much faster. Isabelle is still under
+support many-sorted and higher-order logics. The 1994 version introduced
+greater support for theories. The most important recent change is the
+introduction of the Isar proof language, thanks to Markus Wenzel.
+Isabelle is still under
development and will continue to change.
\subsubsection*{Overview}
@@ -101,7 +114,7 @@
\subsubsection*{Acknowledgements}
Tobias Nipkow contributed most of the section on defining theories.
-Stefan Berghofer and Sara Kalvala suggested improvements.
+Stefan Berghofer, Sara Kalvala and Viktor Kuncak suggested improvements.
Tobias Nipkow has made immense contributions to Isabelle, including the parser
generator, type classes, and the simplifier. Carsten Clasohm and Markus