--- 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