# HG changeset patch
# User wenzelm
# Date 1163514590 -3600
# Node ID f48800c3d573f229405466548f50eb28d31916fb
# Parent  8ebff00544e522598cf528725d03aad5af74c8f2
tuned antiquotation theory;

diff -r 8ebff00544e5 -r f48800c3d573 NEWS
--- 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.
diff -r 8ebff00544e5 -r f48800c3d573 doc-src/IsarRef/syntax.tex
--- 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