doc-src/IsarRef/syntax.tex

 \texttt{(*~\dots~*)} or verbatim text \verb|{*|~\dots~\verb|*}|.
 
 \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
   $no_vars$ operation (see \S\ref{sec:misc-meth-att}) would be particularly
   useful to suppress printing of schematic variables.