actual proofs via \indexref{}{command}{sorry}\hyperlink{command.sorry}{\mbox{\isa{\isacommand{sorry}}}} (see

   actual proofs via \indexref{}{command}{sorry}\hyperlink{command.sorry}{\mbox{\isa{\isacommand{sorry}}}} (see

   \secref{sec:proof-steps}): \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} does not observe the

   \secref{sec:proof-steps}): \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} does not observe the

   proof structure at all, but goes back right to the theory level.

   proof structure at all, but goes back right to the theory level.

   Furthermore, \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} does not produce any result theorem

   Furthermore, \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} does not produce any result theorem

   --- there is no intended claim to be able to complete the proof

   --- there is no intended claim to be able to complete the proof

   A typical application of \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} is to explain Isar proofs

   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

   \emph{within} the system itself, in conjunction with the document

   preparation tools of Isabelle described in \chref{ch:document-prep}.

   preparation tools of Isabelle described in \chref{ch:document-prep}.

   Thus partial or even wrong proof attempts can be discussed in a

   Thus partial or even wrong proof attempts can be discussed in a