doc-src/IsarRef/Thy/document/Proof.tex

   --- there is no intended claim to be able to complete the proof
   anyhow.
 
   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
   the keyword ``\hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}}''.