# HG changeset patch
# User wenzelm
# Date 1124359157 -7200
# Node ID e2bed9e8245493853c8e5db8a8007f825006f404
# Parent  dda6c353b4ce4d241c890a61ff5949c50bf0ad0f
* The ML antiquotation prints type-checked ML expressions verbatim.

diff -r dda6c353b4ce -r e2bed9e82454 NEWS
--- a/NEWS	Thu Aug 18 11:17:51 2005 +0200
+++ b/NEWS	Thu Aug 18 11:59:17 2005 +0200
@@ -83,12 +83,15 @@
   @{term_style style term} and @{thm_style style thm} print a term or
   theorem applying a "style" to it
 
+  @{ML text}
+
 Predefined styles are 'lhs' and 'rhs' printing the lhs/rhs of
 definitions, equations, inequations etc., 'concl' printing only the
 conclusion of a meta-logical statement theorem, and 'prem1' .. 'prem9'
 to print the specified premise.  TermStyle.add_style provides an ML
 interface for introducing further styles.  See also the "LaTeX Sugar"
-document practical applications.
+document practical applications.  The ML antiquotation prints
+type-checked ML expressions verbatim.
 
 * Proper output of proof terms (@{prf ...} and @{full_prf ...}) within
 a proof context.