| changeset 56069 | 451d5b73f8cf |
| parent 55965 | 0c2c61a87a7d |
| child 56071 | 2ffdedb0c044 |
--- a/NEWS Wed Mar 12 21:29:46 2014 +0100 +++ b/NEWS Wed Mar 12 21:58:48 2014 +0100 @@ -437,6 +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. + *** System ***