equal
deleted
inserted
replaced
179 \verb| Toplevel.transition -> Toplevel.transition| \\ |
179 \verb| Toplevel.transition -> Toplevel.transition| \\ |
180 \indexml{Toplevel.theory}\verb|Toplevel.theory: (theory -> theory) ->|\isasep\isanewline% |
180 \indexml{Toplevel.theory}\verb|Toplevel.theory: (theory -> theory) ->|\isasep\isanewline% |
181 \verb| Toplevel.transition -> Toplevel.transition| \\ |
181 \verb| Toplevel.transition -> Toplevel.transition| \\ |
182 \indexml{Toplevel.theory-to-proof}\verb|Toplevel.theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline% |
182 \indexml{Toplevel.theory-to-proof}\verb|Toplevel.theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline% |
183 \verb| Toplevel.transition -> Toplevel.transition| \\ |
183 \verb| Toplevel.transition -> Toplevel.transition| \\ |
|
184 \indexml{Toplevel.theory-to-theory-to-proof}\verb|Toplevel.theory_to_theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline% |
|
185 \verb| Toplevel.transition -> Toplevel.transition| \\ |
184 \indexml{Toplevel.proof}\verb|Toplevel.proof: (Proof.state -> Proof.state) ->|\isasep\isanewline% |
186 \indexml{Toplevel.proof}\verb|Toplevel.proof: (Proof.state -> Proof.state) ->|\isasep\isanewline% |
185 \verb| Toplevel.transition -> Toplevel.transition| \\ |
187 \verb| Toplevel.transition -> Toplevel.transition| \\ |
186 \indexml{Toplevel.proofs}\verb|Toplevel.proofs: (Proof.state -> Proof.state Seq.seq) ->|\isasep\isanewline% |
188 \indexml{Toplevel.proofs}\verb|Toplevel.proofs: (Proof.state -> Proof.state Seq.seq) ->|\isasep\isanewline% |
187 \verb| Toplevel.transition -> Toplevel.transition| \\ |
189 \verb| Toplevel.transition -> Toplevel.transition| \\ |
188 \indexml{Toplevel.proof-to-theory}\verb|Toplevel.proof_to_theory: (Proof.state -> theory) ->|\isasep\isanewline% |
190 \indexml{Toplevel.proof-to-theory}\verb|Toplevel.proof_to_theory: (Proof.state -> theory) ->|\isasep\isanewline% |
205 \item \verb|Toplevel.theory_to_proof| adjoins a global goal function, |
207 \item \verb|Toplevel.theory_to_proof| adjoins a global goal function, |
206 which turns a theory into a proof state. The theory must not be |
208 which turns a theory into a proof state. The theory must not be |
207 changed here! The generic Isar goal setup includes an argument that |
209 changed here! The generic Isar goal setup includes an argument that |
208 specifies how to apply the proven result to the theory, when the |
210 specifies how to apply the proven result to the theory, when the |
209 proof is finished. |
211 proof is finished. |
|
212 |
|
213 \item \verb|Toplevel.theory_to_theory_to_proof| is like \verb|Toplevel.theory_to_proof|, but allows the initial theory to be |
|
214 changed before entering proof state. |
210 |
215 |
211 \item \verb|Toplevel.proof| adjoins a deterministic proof command, |
216 \item \verb|Toplevel.proof| adjoins a deterministic proof command, |
212 with a singleton result state. |
217 with a singleton result state. |
213 |
218 |
214 \item \verb|Toplevel.proofs| adjoins a general proof command, with |
219 \item \verb|Toplevel.proofs| adjoins a general proof command, with |