| changeset 53571 | e58ca0311c0f |
| parent 53371 | 47b23c582127 |
| child 53707 | d1c6bff9ff58 |
--- a/src/Pure/Pure.thy Wed Sep 11 18:52:30 2013 +0200 +++ b/src/Pure/Pure.thy Wed Sep 11 20:16:28 2013 +0200 @@ -68,7 +68,8 @@ and "}" :: prf_close % "proof" and "next" :: prf_block % "proof" and "qed" :: qed_block % "proof" - and "by" ".." "." "done" "sorry" :: "qed" % "proof" + and "by" ".." "." "sorry" :: "qed" % "proof" + and "done" :: "qed_script" % "proof" and "oops" :: qed_global % "proof" and "defer" "prefer" "apply" :: prf_script % "proof" and "apply_end" :: prf_script % "proof" == ""