NEWS
changeset 14919 0f5fde03e2b5
parent 14917 b54b11ebe220
child 14934 bf9f525d4821
     1.1 --- a/NEWS	Thu Jun 10 20:12:49 2004 +0200
     1.2 +++ b/NEWS	Thu Jun 10 20:17:07 2004 +0200
     1.3 @@ -52,8 +52,7 @@
     1.4  * Document preparation: antiquotations now provide the option
     1.5    'locale=NAME' to specify an alternative context used for evaluating
     1.6    and printing the subsequent argument, as in @{thm [locale=LC]
     1.7 -  fold_commute}, for example.  Note that a proof context is escaped to
     1.8 -  the enclosing theory context first.
     1.9 +  fold_commute}, for example.
    1.10  
    1.11  * ML: output via the Isabelle channels of writeln/warning/error
    1.12    etc. is now passed through Output.output, with a hook for arbitrary