--- a/NEWS Tue Nov 14 09:06:08 2006 +0100
+++ b/NEWS Tue Nov 14 15:29:50 2006 +0100
@@ -46,7 +46,8 @@
*** Document preparation ***
* Added antiquotation @{theory name} which prints the name $A$, after
-checking that it refers to a valid theory in the current session.
+checking that it refers to a valid ancestor theory in the current
+context.
* Added antiquotations @{ML_type text} and @{ML_struct text} which
check the given source text as ML type/structure, printing verbatim.
--- a/doc-src/IsarRef/syntax.tex Tue Nov 14 09:06:08 2006 +0100
+++ b/doc-src/IsarRef/syntax.tex Tue Nov 14 15:29:50 2006 +0100
@@ -505,7 +505,7 @@
\begin{descr}
\item [$\at\{theory~A\}$] prints the name $A$, which is guaranteed to
- refer to a valid theory in the current session.
+ refer to a valid ancestor theory in the current context.
\item [$\at\{thm~\vec a\}$] prints theorems $\vec a$. Note that attribute
specifications may be included as well (see also \S\ref{sec:syn-att}); the