NEWS
changeset 56205 ceb8a93460b7
parent 56166 9a241bc276cd
child 56212 3253aaf73a01
     1.1 --- a/NEWS	Tue Mar 18 15:29:58 2014 +0100
     1.2 +++ b/NEWS	Tue Mar 18 16:16:28 2014 +0100
     1.3 @@ -465,10 +465,8 @@
     1.4  theory merge).  Note that the softer Thm.eq_thm_prop is often more
     1.5  appropriate than Thm.eq_thm.
     1.6  
     1.7 -* Simplified programming interface to define ML antiquotations (to
     1.8 -make it more close to the analogous Thy_Output.antiquotation).  See
     1.9 -ML_Context.antiquotation and structure ML_Antiquotation.  Minor
    1.10 -INCOMPATIBILITY.
    1.11 +* Simplified programming interface to define ML antiquotations, see
    1.12 +structure ML_Antiquotation.  Minor INCOMPATIBILITY.
    1.13  
    1.14  * ML antiquotation @{here} refers to its source position, which is
    1.15  occasionally useful for experimentation and diagnostic purposes.