equal
deleted
inserted
replaced
733 \<^descr> @{command "sorry"} is a \<^emph>\<open>fake proof\<close>\index{proof!fake} pretending to |
733 \<^descr> @{command "sorry"} is a \<^emph>\<open>fake proof\<close>\index{proof!fake} pretending to |
734 solve the pending claim without further ado. This only works in interactive |
734 solve the pending claim without further ado. This only works in interactive |
735 development, or if the @{attribute quick_and_dirty} is enabled. Facts |
735 development, or if the @{attribute quick_and_dirty} is enabled. Facts |
736 emerging from fake proofs are not the real thing. Internally, the derivation |
736 emerging from fake proofs are not the real thing. Internally, the derivation |
737 object is tainted by an oracle invocation, which may be inspected via the |
737 object is tainted by an oracle invocation, which may be inspected via the |
738 theorem status @{cite "isabelle-implementation"}. |
738 command @{command "thm_oracles"} (\secref{sec:oracles}). |
739 |
739 |
740 The most important application of @{command "sorry"} is to support |
740 The most important application of @{command "sorry"} is to support |
741 experimentation and top-down proof development. |
741 experimentation and top-down proof development. |
742 |
742 |
743 \<^descr> @{method standard} refers to the default refinement step of some Isar |
743 \<^descr> @{method standard} refers to the default refinement step of some Isar |