--- a/doc-src/Tutorial/basics.tex Thu May 06 11:13:01 1999 +0200
+++ b/doc-src/Tutorial/basics.tex Thu May 06 11:48:09 1999 +0200
@@ -10,16 +10,15 @@
\[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]
We assume that the reader is familiar with the basic concepts of both fields.
For excellent introductions to functional programming consult the textbooks
-by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{Paulson-ML}. Although
+by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}. Although
this tutorial initially concentrates on functional programming, do not be
misled: HOL can express most mathematical concepts, and functional
programming is just one particularly simple and ubiquitous instance.
A tutorial is by definition incomplete. To fully exploit the power of the
-system you need to consult the Isabelle Reference Manual~\cite{Isa-Ref-Man}
-for details about Isabelle and the HOL chapter of the Logics
-manual~\cite{Isa-Logics-Man} for details relating to HOL. Both manuals have a
-comprehensive index.
+system you need to consult the Isabelle Reference Manual~\cite{isabelle-ref}
+for details about Isabelle and the Isabelle/HOL manual~\cite{isabelle-HOL}
+for details relating to HOL. Both manuals have a comprehensive index.
\section{Theories, proofs and interaction}
\label{sec:Basic:Theories}
@@ -58,7 +57,7 @@
This tutorial is concerned with introducing you to the different linguistic
constructs that can fill ${\langle}declarations{\rangle}$ in the above theory template.
A complete grammar of the basic constructs is found in Appendix~A
-of~\cite{Isa-Ref-Man}, for reference in times of doubt.
+of~\cite{isabelle-ref}, for reference in times of doubt.
The tutorial is also concerned with showing you how to prove theorems about
the concepts in a theory. This involves invoking predefined theorem proving