equal
deleted
inserted
replaced
228 |
228 |
229 |
229 |
230 (* local endings *) |
230 (* local endings *) |
231 |
231 |
232 fun local_qed m = Toplevel.proof (Proof.local_qed (m, true)); |
232 fun local_qed m = Toplevel.proof (Proof.local_qed (m, true)); |
233 val local_terminal_proof = Toplevel.proof o Proof.local_terminal_proof; |
233 val local_terminal_proof = Toplevel.proof' o Proof.local_future_terminal_proof; |
234 val local_default_proof = Toplevel.proof Proof.local_default_proof; |
234 val local_default_proof = Toplevel.proof Proof.local_default_proof; |
235 val local_immediate_proof = Toplevel.proof Proof.local_immediate_proof; |
235 val local_immediate_proof = Toplevel.proof Proof.local_immediate_proof; |
236 val local_done_proof = Toplevel.proof Proof.local_done_proof; |
236 val local_done_proof = Toplevel.proof Proof.local_done_proof; |
237 val local_skip_proof = Toplevel.proof' Proof.local_skip_proof; |
237 val local_skip_proof = Toplevel.proof' Proof.local_skip_proof; |
238 |
238 |