NEWS
changeset 14897 577f95db94e4
parent 14885 0a840138dcd7
child 14917 b54b11ebe220
     1.1 --- a/NEWS	Wed Jun 09 18:51:26 2004 +0200
     1.2 +++ b/NEWS	Wed Jun 09 18:52:11 2004 +0200
     1.3 @@ -49,6 +49,12 @@
     1.4  * Pure: tuned internal renaming of symbolic identifiers -- attach
     1.5    primes instead of base 26 numbers.
     1.6  
     1.7 +* Document preparation: antiquotations now provide the option
     1.8 +  'locale=NAME' to specify an alternative context used for evaluating
     1.9 +  and printing the subsequent argument, as in @{thm [locale=LC]
    1.10 +  fold_commute}, for example.  Note that a proof context is escaped to
    1.11 +  the enclosing theory context first.
    1.12 +
    1.13  * ML: all output via channels of writeln/warning/error etc. is now
    1.14    passed through Output.output.  This gives interface builders a
    1.15    chance to adapt text encodings in arbitrary manners (say as XML