--- a/NEWS Thu Oct 28 22:59:33 2010 +0200
+++ b/NEWS Thu Oct 28 23:19:52 2010 +0200
@@ -339,6 +339,10 @@
Fail if the argument is false. Due to inlining the source position of
failed assertions is included in the error output.
+* Discontinued antiquotation @{theory_ref}, which is obsolete since ML
+text is in practice always evaluated with a stable theory checkpoint.
+Minor INCOMPATIBILITY, use (Theory.check_thy @{theory}) instead.
+
* Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its
meaning.