changeset 17117 e2bed9e82454
parent 17097 78f1b66f70a4
child 17139 165c97f9bb63
--- 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.