equal
deleted
inserted
replaced
511 (Scan.succeed (Toplevel.print3 o IsarThy.skip_proof)); |
511 (Scan.succeed (Toplevel.print3 o IsarThy.skip_proof)); |
512 |
512 |
513 val forget_proofP = |
513 val forget_proofP = |
514 OuterSyntax.command "oops" "forget proof" |
514 OuterSyntax.command "oops" "forget proof" |
515 (K.tag_proof K.qed_global) |
515 (K.tag_proof K.qed_global) |
516 (Scan.succeed IsarThy.forget_proof); |
516 (Scan.succeed Toplevel.forget_proof); |
517 |
517 |
518 |
518 |
519 (* proof steps *) |
519 (* proof steps *) |
520 |
520 |
521 val deferP = |
521 val deferP = |