# HG changeset patch
# User nipkow
# Date 925984089 -7200
# Node ID 94b638b3827c220021315a1cdff38d378e2c5214
# Parent  c2754409919b40bc2515bfd60a50903bf495c1d0
Refs.

diff -r c2754409919b -r 94b638b3827c doc-src/Tutorial/basics.tex
--- 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
diff -r c2754409919b -r 94b638b3827c doc-src/Tutorial/fp.tex
--- a/doc-src/Tutorial/fp.tex	Thu May 06 11:13:01 1999 +0200
+++ b/doc-src/Tutorial/fp.tex	Thu May 06 11:48:09 1999 +0200
@@ -382,7 +382,7 @@
 constructor names and $\tau@{ij}$ are types; it is customary to capitalize
 the first letter in constructor names. There are a number of
 restrictions (such as the type should not be empty) detailed
-elsewhere~\cite{Isa-Logics-Man}. Isabelle notifies you if you violate them.
+elsewhere~\cite{isabelle-HOL}. Isabelle notifies you if you violate them.
 
 Laws about datatypes, such as \verb$[] ~= x#xs$ and \texttt{(x\#xs = y\#ys) =
   (x=y \& xs=ys)}, are used automatically during proofs by simplification.
@@ -1068,7 +1068,7 @@
 is commutativity: $x+y = y+x$.  Another example is $(x-y)-z = (x-z)-y$.  Such
 rules are problematic because once they apply, they can be used forever.
 The simplifier is aware of this danger and treats permutative rules
-separately. For details see~\cite{Isa-Ref-Man}.
+separately. For details see~\cite{isabelle-ref}.
 
 \subsubsection{Tracing}
 \indexbold{tracing the simplifier}
@@ -1486,13 +1486,13 @@
 
 For a theoretical analysis of what kinds of datatypes are feasible in HOL
 see, for example,~\cite{Gunter-HOL92}. There are alternatives to pure HOL:
-LCF~\cite{Paulson-LCF} is a logic where types like
+LCF~\cite{paulson87} is a logic where types like
 \begin{ttbox}
 datatype t = C (t -> t)
 \end{ttbox}
 do indeed make sense (note the intentionally different arrow \texttt{->}!).
 There is even a version of LCF on top of HOL, called
-HOLCF~\cite{MuellerNvOS98}.
+HOLCF~\cite{MuellerNvOS99}.
 
 \index{*primrec|)}
 \index{*datatype|)}
@@ -1737,7 +1737,7 @@
 Ackermann's function requires the lexicographic product \texttt{**}:
 \begin{ttbox}
 \input{Recdef/ack}\end{ttbox}
-For details see the manual~\cite{Isa-Logics-Man} and the examples in the
+For details see the manual~\cite{isabelle-HOL} and the examples in the
 library.