--- a/doc-src/Ref/classical.tex Wed May 05 14:31:31 1999 +0200
+++ b/doc-src/Ref/classical.tex Wed May 05 16:44:42 1999 +0200
@@ -112,7 +112,7 @@
theorem and apply rules backwards in a fairly arbitrary manner. This yields a
surprisingly effective proof procedure. Quantifiers add few complications,
since Isabelle handles parameters and schematic variables. See Chapter~10
-of {\em ML for the Working Programmer}~\cite{paulson91} for further
+of {\em ML for the Working Programmer}~\cite{paulson-ml2} for further
discussion.