equal
deleted
inserted
replaced
119 transformer. |
119 transformer. |
120 |
120 |
121 \<^descr> @{ML Toplevel.theory_to_proof}~\<open>tr\<close> adjoins a global |
121 \<^descr> @{ML Toplevel.theory_to_proof}~\<open>tr\<close> adjoins a global |
122 goal function, which turns a theory into a proof state. The theory |
122 goal function, which turns a theory into a proof state. The theory |
123 may be changed before entering the proof; the generic Isar goal |
123 may be changed before entering the proof; the generic Isar goal |
124 setup includes an @{verbatim after_qed} argument that specifies how to |
124 setup includes an \<^verbatim>\<open>after_qed\<close> argument that specifies how to |
125 apply the proven result to the enclosing context, when the proof |
125 apply the proven result to the enclosing context, when the proof |
126 is finished. |
126 is finished. |
127 |
127 |
128 \<^descr> @{ML Toplevel.proof}~\<open>tr\<close> adjoins a deterministic |
128 \<^descr> @{ML Toplevel.proof}~\<open>tr\<close> adjoins a deterministic |
129 proof command, with a singleton result. |
129 proof command, with a singleton result. |