# HG changeset patch
# User haftmann
# Date 1115361459 -7200
# Node ID 8d2fdcc558d1af05177a42571c367b5fd9809ecd
# Parent  145651bc64a83a0f0d371665f4c352e97eeacaf2
added new antiquotations

diff -r 145651bc64a8 -r 8d2fdcc558d1 NEWS
--- a/NEWS	Fri May 06 03:47:44 2005 +0200
+++ b/NEWS	Fri May 06 08:37:39 2005 +0200
@@ -204,8 +204,21 @@
 
 *** Document preparation ***
 
-* New antiquotations @{lhs thm} and @{rhs thm} printing the lhs/rhs of
-  definitions, equations, inequations etc.
+* New antiquotation @{term_type term} printing a term with its
+  type annotated
+
+* New antiquotation @{typeof term} printing the - surprise - the type of 
+  a term
+
+* New antiquotation @{const const} which is the same as @{term const} except
+  that const must be a defined constant identifier; helpful for early detection
+  of typoes
+
+* Two new antiquotations @{term_style style term} and @{thm_style style thm}
+  which print a term / theorem applying a "style" to it; predefined styles
+  are "lhs" and "rhs" printing the lhs/rhs of definitions, equations,
+  inequations etc. and "conclusion" printing only the conclusion of a theorem.
+  More styles may be defined using ML; see the "LaTeX Sugar" document for more
 
 * Antiquotations now provide the option 'locale=NAME' to specify an
   alternative context used for evaluating and printing the subsequent