src/Pure/Pure.thy
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" == ""