--- a/NEWS Wed Mar 12 22:44:55 2014 +0100
+++ b/NEWS Wed Mar 12 22:57:50 2014 +0100
@@ -437,9 +437,10 @@
theory merge). Note that the softer Thm.eq_thm_prop is often more
appropriate than Thm.eq_thm.
-* Simplified programming interface to define ML antiquotations, see
-ML_Context.antiquotation, to make it more close to the analogous
-Thy_Output.antiquotation. Minor INCOMPATIBILTY.
+* Simplified programming interface to define ML antiquotations (to
+make it more close to the analogous Thy_Output.antiquotation). See
+ML_Context.antiquotation and structure ML_Antiquotation. Minor
+INCOMPATIBILITY.
* ML antiquotation @{here} refers to its source position, which is
occasionally useful for experimentation and diagnostic purposes.