equal
deleted
inserted
replaced
690 Outer_Syntax.command @{command_spec "sorry"} "skip proof (quick-and-dirty mode only!)" |
690 Outer_Syntax.command @{command_spec "sorry"} "skip proof (quick-and-dirty mode only!)" |
691 (Scan.succeed Isar_Cmd.skip_proof); |
691 (Scan.succeed Isar_Cmd.skip_proof); |
692 |
692 |
693 val _ = |
693 val _ = |
694 Outer_Syntax.command @{command_spec "oops"} "forget proof" |
694 Outer_Syntax.command @{command_spec "oops"} "forget proof" |
695 (Scan.succeed Toplevel.forget_proof); |
695 (Scan.succeed (Toplevel.forget_proof true)); |
696 |
696 |
697 |
697 |
698 (* proof steps *) |
698 (* proof steps *) |
699 |
699 |
700 val _ = |
700 val _ = |