--- a/doc-src/IsarRef/Thy/document/Proof.tex Tue Nov 18 18:22:49 2008 +0100
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Tue Nov 18 18:25:10 2008 +0100
@@ -128,7 +128,7 @@
A typical application of \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} is to explain Isar proofs
\emph{within} the system itself, in conjunction with the document
- preparation tools of Isabelle described in \cite{isabelle-sys}.
+ preparation tools of Isabelle described in \chref{ch:document-prep}.
Thus partial or even wrong proof attempts can be discussed in a
logically sound manner. Note that the Isabelle {\LaTeX} macros can
be easily adapted to print something like ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' instead of