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