--- a/NEWS Thu Jun 10 20:12:49 2004 +0200
+++ b/NEWS Thu Jun 10 20:17:07 2004 +0200
@@ -52,8 +52,7 @@
* 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.
+ fold_commute}, for example.
* ML: output via the Isabelle channels of writeln/warning/error
etc. is now passed through Output.output, with a hook for arbitrary
--- a/doc-src/IsarRef/syntax.tex Thu Jun 10 20:12:49 2004 +0200
+++ b/doc-src/IsarRef/syntax.tex Thu Jun 10 20:17:07 2004 +0200
@@ -532,8 +532,7 @@
\item[$goals_limit = nat$] determines the maximum number of goals to be
printed.
\item[$locale = name$] specifies an alternative context used for evaluating
- and printing the subsequent argument. Note that a proof context is escaped
- to the enclosing theory context first.
+ and printing the subsequent argument.
\end{descr}
For boolean flags, ``$name = true$'' may be abbreviated as ``$name$''. All of