diff -r 985133486546 -r 577f95db94e4 NEWS
--- a/NEWS	Wed Jun 09 18:51:26 2004 +0200
+++ b/NEWS	Wed Jun 09 18:52:11 2004 +0200
@@ -49,6 +49,12 @@
 * Pure: tuned internal renaming of symbolic identifiers -- attach
   primes instead of base 26 numbers.
 
+* Document preparation: antiquotations now provide the option
+  'locale=NAME' to specify an alternative context used for evaluating
+  and printing the subsequent argument, as in @{thm [locale=LC]
+  fold_commute}, for example.  Note that a proof context is escaped to
+  the enclosing theory context first.
+
 * ML: all output via channels of writeln/warning/error etc. is now
   passed through Output.output.  This gives interface builders a
   chance to adapt text encodings in arbitrary manners (say as XML