equal
deleted
inserted
replaced
127 actual proofs via @{command_ref "sorry"} (see |
127 actual proofs via @{command_ref "sorry"} (see |
128 \secref{sec:proof-steps}): @{command "oops"} does not observe the |
128 \secref{sec:proof-steps}): @{command "oops"} does not observe the |
129 proof structure at all, but goes back right to the theory level. |
129 proof structure at all, but goes back right to the theory level. |
130 Furthermore, @{command "oops"} does not produce any result theorem |
130 Furthermore, @{command "oops"} does not produce any result theorem |
131 --- there is no intended claim to be able to complete the proof |
131 --- there is no intended claim to be able to complete the proof |
132 anyhow. |
132 in any way. |
133 |
133 |
134 A typical application of @{command "oops"} is to explain Isar proofs |
134 A typical application of @{command "oops"} is to explain Isar proofs |
135 \emph{within} the system itself, in conjunction with the document |
135 \emph{within} the system itself, in conjunction with the document |
136 preparation tools of Isabelle described in \chref{ch:document-prep}. |
136 preparation tools of Isabelle described in \chref{ch:document-prep}. |
137 Thus partial or even wrong proof attempts can be discussed in a |
137 Thus partial or even wrong proof attempts can be discussed in a |