diff -r 6a753a6d6738 -r c120262044b6 doc-src/Intro/foundations.tex
--- a/doc-src/Intro/foundations.tex	Wed May 05 14:31:31 1999 +0200
+++ b/doc-src/Intro/foundations.tex	Wed May 05 16:44:42 1999 +0200
@@ -959,7 +959,7 @@
 rather than on individual subgoals.  An Isabelle tactic is a function that
 takes a proof state and returns a sequence (lazy list) of possible
 successor states.  Lazy lists are coded in ML as functions, a standard
-technique~\cite{paulson91}.  Isabelle represents proof states by theorems.
+technique~\cite{paulson-ml2}.  Isabelle represents proof states by theorems.
 
 Basic tactics execute the meta-rules described above, operating on a
 given subgoal.  The {\bf resolution tactics} take a list of rules and