changeset 62312 | 5e5a881ebc12 |
parent 62169 | a6047f511de7 |
child 62490 | 39d01eaf5292 |
--- a/src/Pure/Pure.thy Sun Feb 14 16:29:30 2016 +0100 +++ b/src/Pure/Pure.thy Sun Feb 14 16:30:27 2016 +0100 @@ -64,7 +64,7 @@ and "}" :: prf_close % "proof" and "next" :: next_block % "proof" and "qed" :: qed_block % "proof" - and "by" ".." "." "sorry" :: "qed" % "proof" + and "by" ".." "." "sorry" "\<proof>" :: "qed" % "proof" and "done" :: "qed_script" % "proof" and "oops" :: qed_global % "proof" and "defer" "prefer" "apply" :: prf_script % "proof"