| changeset 61597 | 53e32a9b66b8 |
| parent 61595 | 3591274c607e |
| child 61600 | 1ca11ddfcc70 |
--- a/NEWS Sat Nov 07 00:28:42 2015 +0100 +++ b/NEWS Sat Nov 07 12:53:22 2015 +0100 @@ -502,6 +502,8 @@ *** ML *** +* Antiquotation @{undefined} or \<^undefined> inlines (raise Match). + * The auxiliary module Pure/display.ML has been eliminated. Its elementary thm print operations are now in Pure/more_thm.ML and thus called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY.